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.

Locally finite order etc instances #

source
instance Fin.instLocallyFiniteOrder (n : ℕ) :
LocallyFiniteOrder (Fin n)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Fin.instLocallyFiniteOrderBot (n : ℕ) :
LocallyFiniteOrderBot (Fin n)
Equations
source
instance Fin.instLocallyFiniteOrderTop (n : ℕ) :
LocallyFiniteOrderTop (Fin n)
Equations
source
@[simp]
theorem Fin.attachFin_Icc {n : ℕ} (a b : Fin n) :
(Finset.Icc ↑a ↑b).attachFin ⋯ = Finset.Icc a b
source
@[simp]
theorem Fin.attachFin_Ico {n : ℕ} (a b : Fin n) :
(Finset.Ico ↑a ↑b).attachFin ⋯ = Finset.Ico a b
source
@[simp]
theorem Fin.attachFin_Ioc {n : ℕ} (a b : Fin n) :
(Finset.Ioc ↑a ↑b).attachFin ⋯ = Finset.Ioc a b
source
@[simp]
theorem Fin.attachFin_Ioo {n : ℕ} (a b : Fin n) :
(Finset.Ioo ↑a ↑b).attachFin ⋯ = Finset.Ioo a b
source
@[simp]
theorem Fin.attachFin_uIcc {n : ℕ} (a b : Fin n) :
(Finset.uIcc ↑a ↑b).attachFin ⋯ = Finset.uIcc a b
source
@[simp]
theorem Fin.attachFin_Iic {n : ℕ} (a : Fin n) :
(Finset.Iic ↑a).attachFin ⋯ = Finset.Iic a
source
@[simp]
theorem Fin.attachFin_Ico_eq_Ici {n : ℕ} (a : Fin n) :
(Finset.Ico (↑a) n).attachFin ⋯ = Finset.Ici a
source
@[simp]
theorem Fin.attachFin_Iio {n : ℕ} (a : Fin n) :
(Finset.Iio ↑a).attachFin ⋯ = Finset.Iio a
source
@[simp]
theorem Fin.attachFin_Ioo_eq_Ioi {n : ℕ} (a : Fin n) :
(Finset.Ioo (↑a) n).attachFin ⋯ = Finset.Ioi a
source
@[deprecated Fin.attachFin_Icc (since := "2025-04-06")]
theorem Fin.Icc_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Icc a b = Finset.fin n (Finset.Icc ↑a ↑b)
source
@[deprecated Fin.attachFin_Ico (since := "2025-04-06")]
theorem Fin.Ico_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Ico a b = Finset.fin n (Finset.Ico ↑a ↑b)
source
@[deprecated Fin.attachFin_Ioc (since := "2025-04-06")]
theorem Fin.Ioc_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Ioc a b = Finset.fin n (Finset.Ioc ↑a ↑b)
source
@[deprecated Fin.attachFin_Ioo (since := "2025-04-06")]
theorem Fin.Ioo_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.Ioo a b = Finset.fin n (Finset.Ioo ↑a ↑b)
source
@[deprecated Fin.attachFin_uIcc (since := "2025-04-06")]
theorem Fin.uIcc_eq_finset_subtype {n : ℕ} (a b : Fin n) :
Finset.uIcc a b = Finset.fin n (Finset.uIcc ↑a ↑b)
source
@[deprecated Fin.attachFin_Ico_eq_Ici (since := "2025-04-06")]
theorem Fin.Ici_eq_finset_subtype {n : ℕ} (a : Fin n) :
Finset.Ici a = Finset.fin n (Finset.Ico (↑a) n)
source
@[deprecated Fin.attachFin_Ioo_eq_Ioi (since := "2025-04-06")]
theorem Fin.Ioi_eq_finset_subtype {n : ℕ} (a : Fin n) :
Finset.Ioi a = Finset.fin n (Finset.Ioo (↑a) n)
source
@[deprecated Fin.attachFin_Iic (since := "2025-04-06")]
theorem Fin.Iic_eq_finset_subtype {n : ℕ} (b : Fin n) :
Finset.Iic b = Finset.fin n (Finset.Iic ↑b)
source
@[deprecated Fin.attachFin_Iio (since := "2025-04-06")]
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_Icc {n : ℕ} (a b : Fin n) :
Finset.map valEmbedding (Finset.Icc a b) = Finset.Icc ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Ico {n : ℕ} (a b : Fin n) :
Finset.map valEmbedding (Finset.Ico a b) = Finset.Ico ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Ioc {n : ℕ} (a b : Fin n) :
Finset.map valEmbedding (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Ioo {n : ℕ} (a b : Fin n) :
Finset.map valEmbedding (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
source
@[simp]
theorem Fin.map_valEmbedding_uIcc {n : ℕ} (a b : Fin n) :
Finset.map valEmbedding (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
source
@[deprecated Fin.map_valEmbedding_uIcc (since := "2025-04-08")]
theorem Fin.map_subtype_embedding_uIcc {n : ℕ} (a b : Fin n) :
Finset.map valEmbedding (Finset.uIcc a b) = Finset.uIcc ↑a ↑b

Alias of Fin.map_valEmbedding_uIcc.

source
@[simp]
theorem Fin.map_valEmbedding_Ici {n : ℕ} (a : Fin n) :
Finset.map valEmbedding (Finset.Ici a) = Finset.Ico (↑a) n
source
@[simp]
theorem Fin.map_valEmbedding_Ioi {n : ℕ} (a : Fin n) :
Finset.map valEmbedding (Finset.Ioi a) = Finset.Ioo (↑a) n
source
@[simp]
theorem Fin.map_valEmbedding_Iic {n : ℕ} (b : Fin n) :
Finset.map valEmbedding (Finset.Iic b) = Finset.Iic ↑b
source
@[simp]
theorem Fin.map_valEmbedding_Iio {n : ℕ} (b : Fin n) :
Finset.map valEmbedding (Finset.Iio b) = Finset.Iio ↑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
@[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
@[deprecated Fintype.card_Icc (since := "2025-03-28")]
theorem Fin.card_fintypeIcc {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
source
@[deprecated Fintype.card_Ico (since := "2025-03-28")]
theorem Fin.card_fintypeIco {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
source
@[deprecated Fintype.card_Ioc (since := "2025-03-28")]
theorem Fin.card_fintypeIoc {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
source
@[deprecated Fintype.card_Ioo (since := "2025-03-28")]
theorem Fin.card_fintypeIoo {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
source
@[deprecated Fintype.card_uIcc (since := "2025-03-28")]
theorem Fin.card_fintype_uIcc {n : ℕ} (a b : Fin n) :
Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1
source
@[deprecated Fintype.card_Ici (since := "2025-03-28")]
theorem Fin.card_fintypeIci {n : ℕ} (a : Fin n) :
Fintype.card ↑(Set.Ici a) = n - ↑a
source
@[deprecated Fintype.card_Ioi (since := "2025-03-28")]
theorem Fin.card_fintypeIoi {n : ℕ} (a : Fin n) :
Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a
source
@[deprecated Fintype.card_Iic (since := "2025-03-28")]
theorem Fin.card_fintypeIic {n : ℕ} (b : Fin n) :
Fintype.card ↑(Set.Iic b) = ↑b + 1
source
@[deprecated Fintype.card_Iio (since := "2025-03-28")]
theorem Fin.card_fintypeIio {n : ℕ} (b : Fin n) :
Fintype.card ↑(Set.Iio b) = ↑b