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
Equations
• = Fin.orderIsoSubtype.locallyFiniteOrder
Equations
• = Fin.orderIsoSubtype.locallyFiniteOrderBot
Equations
• = match x with | 0 => IsEmpty.toLocallyFiniteOrderTop | n.succ => inferInstance
theorem Fin.Icc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Icc a b)
theorem Fin.Ico_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Ico a b)
theorem Fin.Ioc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Ioc a b)
theorem Fin.Ioo_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Ioo a b)
theorem Fin.uIcc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.uIcc a b)
@[simp]
theorem Fin.map_valEmbedding_Icc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = 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
@[simp]
theorem Fin.map_valEmbedding_Ioc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = 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
@[simp]
theorem Fin.map_subtype_embedding_uIcc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = Finset.uIcc a b
@[simp]
theorem Fin.card_Icc {n : } (a : Fin n) (b : Fin n) :
().card = b + 1 - a
@[simp]
theorem Fin.card_Ico {n : } (a : Fin n) (b : Fin n) :
().card = b - a
@[simp]
theorem Fin.card_Ioc {n : } (a : Fin n) (b : Fin n) :
().card = b - a
@[simp]
theorem Fin.card_Ioo {n : } (a : Fin n) (b : Fin n) :
().card = b - a - 1
@[simp]
theorem Fin.card_uIcc {n : } (a : Fin n) (b : Fin n) :
().card = (b - a).natAbs + 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) = (b - a).natAbs + 1
theorem Fin.Ici_eq_finset_subtype {n : } (a : Fin n) :
= Finset.fin n (Finset.Icc (a) n)
theorem Fin.Ioi_eq_finset_subtype {n : } (a : Fin n) :
= Finset.fin n (Finset.Ioc (a) n)
theorem Fin.Iic_eq_finset_subtype {n : } (b : Fin n) :
theorem Fin.Iio_eq_finset_subtype {n : } (b : Fin n) :
@[simp]
theorem Fin.map_valEmbedding_Ici {n : } (a : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Icc (a) (n - 1)
@[simp]
theorem Fin.map_valEmbedding_Ioi {n : } (a : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Ioc (a) (n - 1)
@[simp]
theorem Fin.map_valEmbedding_Iic {n : } (b : Fin n) :
Finset.map Fin.valEmbedding () =
@[simp]
theorem Fin.map_valEmbedding_Iio {n : } (b : Fin n) :
Finset.map Fin.valEmbedding () =
@[simp]
theorem Fin.card_Ici {n : } (a : Fin n) :
().card = n - a
@[simp]
theorem Fin.card_Ioi {n : } (a : Fin n) :
().card = n - 1 - a
@[simp]
theorem Fin.card_Iic {n : } (b : Fin n) :
().card = b + 1
@[simp]
theorem Fin.card_Iio {n : } (b : Fin n) :
().card = b
theorem Fin.card_fintypeIci {n : } (a : Fin n) :
Fintype.card () = n - a
theorem Fin.card_fintypeIoi {n : } (a : Fin n) :
Fintype.card () = n - 1 - a
theorem Fin.card_fintypeIic {n : } (b : Fin n) :
Fintype.card () = b + 1
theorem Fin.card_fintypeIio {n : } (b : Fin n) :
Fintype.card () = b