HepLean Documentation

Mathlib.Order.Interval.Finset.Fin

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.

source
@[simp]
theorem Fin.coe_sup {n : ℕ} (a b : Fin n) :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[simp]
theorem Fin.coe_inf {n : ℕ} (a b : Fin n) :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
@[simp]
theorem Fin.coe_max {n : ℕ} (a b : Fin n) :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[simp]
theorem Fin.coe_min {n : ℕ} (a b : Fin n) :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
instance Fin.instLocallyFiniteOrder (n : ℕ) :
LocallyFiniteOrder (Fin n)
Equations
source
instance Fin.instLocallyFiniteOrderBot (n : ℕ) :
LocallyFiniteOrderBot (Fin n)
Equations
source
instance Fin.instLocallyFiniteOrderTop (n : ℕ) :
LocallyFiniteOrderTop (Fin n)
Equations
source
theorem Fin.Icc_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Icc a b = Finset.fin n (Finset.Icc ↑a ↑b)
source
theorem Fin.Ico_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Ico a b = Finset.fin n (Finset.Ico ↑a ↑b)
source
theorem Fin.Ioc_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Ioc a b = Finset.fin n (Finset.Ioc ↑a ↑b)
source
theorem Fin.Ioo_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Ioo a b = Finset.fin n (Finset.Ioo ↑a ↑b)
source
theorem Fin.uIcc_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.uIcc a b = Finset.fin n (Finset.uIcc ↑a ↑b)
source
@[simp]
theorem Fin.map_valEmbedding_Icc {n : ℕ} (a b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Icc a b) = Finset.Icc ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Ico {n : ℕ} (a b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ico a b) = Finset.Ico ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Ioc {n : ℕ} (a b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Ioo {n : ℕ} (a b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
source
@[simp]
theorem Fin.map_subtype_embedding_uIcc {n : ℕ} (a b : Fin n) :
Finset.map Fin.valEmbedding (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
source
@[simp]
theorem Fin.card_Icc {n : ℕ} (a b : Fin n) :
(Finset.Icc a b).card = ↑b + 1 - ↑a
source
@[simp]
theorem Fin.card_Ico {n : ℕ} (a b : Fin n) :
(Finset.Ico a b).card = ↑b - ↑a
source
@[simp]
theorem Fin.card_Ioc {n : ℕ} (a b : Fin n) :
(Finset.Ioc a b).card = ↑b - ↑a
source
@[simp]
theorem Fin.card_Ioo {n : ℕ} (a b : Fin n) :
(Finset.Ioo a b).card = ↑b - ↑a - 1
source
@[simp]
theorem Fin.card_uIcc {n : ℕ} (a b : Fin n) :
(Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
source
theorem Fin.card_fintypeIcc {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
source
theorem Fin.card_fintypeIco {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
source
theorem Fin.card_fintypeIoc {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
source
theorem Fin.card_fintypeIoo {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
source
theorem Fin.card_fintype_uIcc {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1
source
theorem Fin.Ici_eq_finset_subtype {n : ℕ} (a : Fin n) :
Finset.Ici a = Finset.fin n (Finset.Icc (↑a) n)
source
theorem Fin.Ioi_eq_finset_subtype {n : ℕ} (a : Fin n) :
Finset.Ioi a = Finset.fin n (Finset.Ioc (↑a) n)
source
theorem Fin.Iic_eq_finset_subtype {n : ℕ} (b : Fin n) :
Finset.Iic b = Finset.fin n (Finset.Iic ↑b)
source
theorem Fin.Iio_eq_finset_subtype {n : ℕ} (b : Fin n) :
Finset.Iio b = Finset.fin n (Finset.Iio ↑b)
source
@[simp]
theorem Fin.map_valEmbedding_Ici {n : ℕ} (a : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ici a) = Finset.Icc (↑a) (n - 1)
source
@[simp]
theorem Fin.map_valEmbedding_Ioi {n : ℕ} (a : Fin n) :
Finset.map Fin.valEmbedding (Finset.Ioi a) = Finset.Ioc (↑a) (n - 1)
source
@[simp]
theorem Fin.map_valEmbedding_Iic {n : ℕ} (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Iic b) = Finset.Iic ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Iio {n : ℕ} (b : Fin n) :
Finset.map Fin.valEmbedding (Finset.Iio b) = Finset.Iio ↑b
source
@[simp]
theorem Fin.card_Ici {n : ℕ} (a : Fin n) :
(Finset.Ici a).card = n - ↑a
source
@[simp]
theorem Fin.card_Ioi {n : ℕ} (a : Fin n) :
(Finset.Ioi a).card = n - 1 - ↑a
source
@[simp]
theorem Fin.card_Iic {n : ℕ} (b : Fin n) :
(Finset.Iic b).card = ↑b + 1
source
@[simp]
theorem Fin.card_Iio {n : ℕ} (b : Fin n) :
(Finset.Iio b).card = ↑b
source
theorem Fin.card_fintypeIci {n : ℕ} (a : Fin n) :
Fintype.card ↑(Set.Ici a) = n - ↑a
source
theorem Fin.card_fintypeIoi {n : ℕ} (a : Fin n) :
Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a
source
theorem Fin.card_fintypeIic {n : ℕ} (b : Fin n) :
Fintype.card ↑(Set.Iic b) = ↑b + 1
source
theorem Fin.card_fintypeIio {n : ℕ} (b : Fin n) :
Fintype.card ↑(Set.Iio b) = ↑b