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.

instance Fin.instLocallyFiniteOrder (n : ℕ) :

LocallyFiniteOrder (Fin n)

Equations

Fin.instLocallyFiniteOrder n = Fin.orderIsoSubtype.locallyFiniteOrder

instance Fin.instLocallyFiniteOrderBot (n : ℕ) :

LocallyFiniteOrderBot (Fin n)

Equations

Fin.instLocallyFiniteOrderBot n = Fin.orderIsoSubtype.locallyFiniteOrderBot

instance Fin.instLocallyFiniteOrderTop (n : ℕ) :

LocallyFiniteOrderTop (Fin n)

Equations

theorem Fin.Icc_eq_finset_subtype {n : ℕ} (a b : Fin n) :

Finset.Icc a b = Finset.fin n (Finset.Icc ↑a ↑b)

theorem Fin.Ico_eq_finset_subtype {n : ℕ} (a b : Fin n) :

Finset.Ico a b = Finset.fin n (Finset.Ico ↑a ↑b)

theorem Fin.Ioc_eq_finset_subtype {n : ℕ} (a b : Fin n) :

Finset.Ioc a b = Finset.fin n (Finset.Ioc ↑a ↑b)

theorem Fin.Ioo_eq_finset_subtype {n : ℕ} (a b : Fin n) :

Finset.Ioo a b = Finset.fin n (Finset.Ioo ↑a ↑b)

theorem Fin.uIcc_eq_finset_subtype {n : ℕ} (a b : Fin n) :

Finset.uIcc a b = Finset.fin n (Finset.uIcc ↑a ↑b)

@[simp]

theorem Fin.map_valEmbedding_Icc {n : ℕ} (a b : Fin n) :

Finset.map valEmbedding (Finset.Icc a b) = Finset.Icc ↑a ↑b

@[simp]

theorem Fin.map_valEmbedding_Ico {n : ℕ} (a b : Fin n) :

Finset.map valEmbedding (Finset.Ico a b) = Finset.Ico ↑a ↑b

@[simp]

theorem Fin.map_valEmbedding_Ioc {n : ℕ} (a b : Fin n) :

Finset.map valEmbedding (Finset.Ioc a b) = Finset.Ioc ↑a ↑b

@[simp]

theorem Fin.map_valEmbedding_Ioo {n : ℕ} (a b : Fin n) :

Finset.map valEmbedding (Finset.Ioo a b) = Finset.Ioo ↑a ↑b

@[simp]

theorem Fin.map_subtype_embedding_uIcc {n : ℕ} (a b : Fin n) :

Finset.map valEmbedding (Finset.uIcc a b) = Finset.uIcc ↑a ↑b

@[simp]

theorem Fin.card_Icc {n : ℕ} (a b : Fin n) :

(Finset.Icc a b).card = ↑b + 1 - ↑a

@[simp]

theorem Fin.card_Ico {n : ℕ} (a b : Fin n) :

(Finset.Ico a b).card = ↑b - ↑a

@[simp]

theorem Fin.card_Ioc {n : ℕ} (a b : Fin n) :

(Finset.Ioc a b).card = ↑b - ↑a

@[simp]

theorem Fin.card_Ioo {n : ℕ} (a b : Fin n) :

(Finset.Ioo a b).card = ↑b - ↑a - 1

@[simp]

theorem Fin.card_uIcc {n : ℕ} (a b : Fin n) :

(Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1

theorem Fin.card_fintypeIcc {n : ℕ} (a b : Fin n) :

Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a

theorem Fin.card_fintypeIco {n : ℕ} (a b : Fin n) :

Fintype.card ↑(Set.Ico a b) = ↑b - ↑a

theorem Fin.card_fintypeIoc {n : ℕ} (a b : Fin n) :

Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a

theorem Fin.card_fintypeIoo {n : ℕ} (a b : Fin n) :

Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1

theorem Fin.card_fintype_uIcc {n : ℕ} (a b : Fin n) :

Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 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 valEmbedding (Finset.Ici a) = Finset.Icc (↑a) (n - 1)

@[simp]

theorem Fin.map_valEmbedding_Ioi {n : ℕ} (a : Fin n) :

Finset.map valEmbedding (Finset.Ioi a) = Finset.Ioc (↑a) (n - 1)

@[simp]

theorem Fin.map_valEmbedding_Iic {n : ℕ} (b : Fin n) :

Finset.map valEmbedding (Finset.Iic b) = Finset.Iic ↑b

@[simp]

theorem Fin.map_valEmbedding_Iio {n : ℕ} (b : Fin n) :

Finset.map 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