Documentation

Mathlib.Data.Fin.Interval

Finite intervals in Fin n #

This file proves that Fin n is a LocallyFiniteOrder and calculates the cardinality of its intervals as Finsets and Fintypes.

@[simp]
theorem Fin.coe_sup {n : } (a : Fin n) (b : Fin n) :
(a b) = a b
@[simp]
theorem Fin.coe_inf {n : } (a : Fin n) (b : Fin n) :
(a b) = a b
@[simp]
theorem Fin.coe_max {n : } (a : Fin n) (b : Fin n) :
(max a b) = max a b
@[simp]
theorem Fin.coe_min {n : } (a : Fin n) (b : Fin n) :
(min a b) = min a b
theorem Fin.Icc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
Finset.Icc a b = Finset.fin n (Finset.Icc a b)
theorem Fin.Ico_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
Finset.Ico a b = Finset.fin n (Finset.Ico a b)
theorem Fin.Ioc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
Finset.Ioc a b = Finset.fin n (Finset.Ioc a b)
theorem Fin.Ioo_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
Finset.Ioo a b = Finset.fin n (Finset.Ioo a b)
theorem Fin.uIcc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
@[simp]
theorem Fin.map_valEmbedding_Icc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Icc a b) = Finset.Icc a b
@[simp]
theorem Fin.map_valEmbedding_Ico {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ico a b) = Finset.Ico a b
@[simp]
theorem Fin.map_valEmbedding_Ioc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ioc a b) = Finset.Ioc a b
@[simp]
theorem Fin.map_valEmbedding_Ioo {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ioo a b) = Finset.Ioo a b
@[simp]
theorem Fin.map_subtype_embedding_uIcc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.uIcc a b) = Finset.uIcc a b
@[simp]
theorem Fin.card_Icc {n : } (a : Fin n) (b : Fin n) :
(Finset.Icc a b).card = b + 1 - a
@[simp]
theorem Fin.card_Ico {n : } (a : Fin n) (b : Fin n) :
(Finset.Ico a b).card = b - a
@[simp]
theorem Fin.card_Ioc {n : } (a : Fin n) (b : Fin n) :
(Finset.Ioc a b).card = b - a
@[simp]
theorem Fin.card_Ioo {n : } (a : Fin n) (b : Fin n) :
(Finset.Ioo a b).card = b - a - 1
@[simp]
theorem Fin.card_uIcc {n : } (a : Fin n) (b : Fin n) :
(Finset.uIcc a b).card = Int.natAbs (b - a) + 1
theorem Fin.card_fintypeIcc {n : } (a : Fin n) (b : Fin n) :
Fintype.card (Set.Icc a b) = b + 1 - a
theorem Fin.card_fintypeIco {n : } (a : Fin n) (b : Fin n) :
Fintype.card (Set.Ico a b) = b - a
theorem Fin.card_fintypeIoc {n : } (a : Fin n) (b : Fin n) :
Fintype.card (Set.Ioc a b) = b - a
theorem Fin.card_fintypeIoo {n : } (a : Fin n) (b : Fin n) :
Fintype.card (Set.Ioo a b) = b - a - 1
theorem Fin.card_fintype_uIcc {n : } (a : Fin n) (b : Fin n) :
Fintype.card (Set.uIcc a b) = Int.natAbs (b - a) + 1
@[simp]
theorem Fin.map_valEmbedding_Ici {n : } (a : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ici a) = Finset.Icc (a) (n - 1)
@[simp]
theorem Fin.map_valEmbedding_Ioi {n : } (a : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ioi a) = Finset.Ioc (a) (n - 1)
@[simp]
theorem Fin.map_valEmbedding_Iic {n : } (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Iic b) = Finset.Iic b
@[simp]
theorem Fin.map_valEmbedding_Iio {n : } (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Iio b) = Finset.Iio b
@[simp]
theorem Fin.card_Ici {n : } (a : Fin n) :
(Finset.Ici a).card = n - a
@[simp]
theorem Fin.card_Ioi {n : } (a : Fin n) :
(Finset.Ioi a).card = n - 1 - a
@[simp]
theorem Fin.card_Iic {n : } (b : Fin n) :
(Finset.Iic b).card = b + 1
@[simp]
theorem Fin.card_Iio {n : } (b : Fin n) :
(Finset.Iio b).card = b
theorem Fin.card_fintypeIci {n : } (a : Fin n) :
Fintype.card (Set.Ici a) = n - a
theorem Fin.card_fintypeIoi {n : } (a : Fin n) :
Fintype.card (Set.Ioi a) = n - 1 - a
theorem Fin.card_fintypeIic {n : } (b : Fin n) :
Fintype.card (Set.Iic b) = b + 1
theorem Fin.card_fintypeIio {n : } (b : Fin n) :
Fintype.card (Set.Iio b) = b