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

instance Fin.instLocallyFiniteOrder (n : ℕ) : LocallyFiniteOrder (Fin n)

Equations

• Fin.instLocallyFiniteOrder n = OrderIso.locallyFiniteOrder Fin.orderIsoSubtype

instance Fin.instLocallyFiniteOrderBot (n : ℕ) : LocallyFiniteOrderBot (Fin n)

Equations

• Fin.instLocallyFiniteOrderBot n = OrderIso.locallyFiniteOrderBot Fin.orderIsoSubtype

instance Fin.instLocallyFiniteOrderTop (n : ℕ) : LocallyFiniteOrderTop (Fin n)

Equations

• Fin.instLocallyFiniteOrderTop x = match x with | 0 => IsEmpty.toLocallyFiniteOrderTop | Nat.succ n => inferInstance

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) : Finset.uIcc a b = 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) = 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

theorem Fin.Ici_eq_finset_subtype {n : ℕ} (a : Fin n) : Finset.Ici a = Finset.fin n (Finset.Icc (↑a) n)

theorem Fin.Ioi_eq_finset_subtype {n : ℕ} (a : Fin n) : Finset.Ioi a = Finset.fin n (Finset.Ioc (↑a) n)

theorem Fin.Iic_eq_finset_subtype {n : ℕ} (b : Fin n) : Finset.Iic b = Finset.fin n (Finset.Iic ↑b)

theorem Fin.Iio_eq_finset_subtype {n : ℕ} (b : Fin n) : Finset.Iio b = Finset.fin n (Finset.Iio ↑b)

@[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