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_Ico_eq_Ici {n : ℕ} (a : Fin n) :
(Finset.Ico (↑a) n).attachFin ⋯ = Finset.Ici a
source
@[simp]
theorem Fin.attachFin_Ioo_eq_Ioi {n : ℕ} (a : Fin n) :
(Finset.Ioo (↑a) n).attachFin ⋯ = Finset.Ioi a
source
@[simp]
theorem Fin.attachFin_Iic {n : ℕ} (a : Fin n) :
(Finset.Iic ↑a).attachFin ⋯ = Finset.Iic a
source
@[simp]
theorem Fin.attachFin_Iio {n : ℕ} (a : Fin n) :
(Finset.Iio ↑a).attachFin ⋯ = Finset.Iio 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)

Images under Fin.val #

source
@[simp]
theorem Fin.finsetImage_val_Icc {n : ℕ} (a b : Fin n) :
Finset.image val (Finset.Icc a b) = Finset.Icc ↑a ↑b
source
@[simp]
theorem Fin.finsetImage_val_Ico {n : ℕ} (a b : Fin n) :
Finset.image val (Finset.Ico a b) = Finset.Ico ↑a ↑b
source
@[simp]
theorem Fin.finsetImage_val_Ioc {n : ℕ} (a b : Fin n) :
Finset.image val (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
source
@[simp]
theorem Fin.finsetImage_val_Ioo {n : ℕ} (a b : Fin n) :
Finset.image val (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
source
@[simp]
theorem Fin.finsetImage_val_uIcc {n : ℕ} (a b : Fin n) :
Finset.image val (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
source
@[simp]
theorem Fin.finsetImage_val_Ici {n : ℕ} (a : Fin n) :
Finset.image val (Finset.Ici a) = Finset.Ico (↑a) n
source
@[simp]
theorem Fin.finsetImage_val_Ioi {n : ℕ} (a : Fin n) :
Finset.image val (Finset.Ioi a) = Finset.Ioo (↑a) n
source
@[simp]
theorem Fin.finsetImage_val_Iic {n : ℕ} (a : Fin n) :
Finset.image val (Finset.Iic a) = Finset.Iic ↑a
source
@[simp]
theorem Fin.finsetImage_val_Iio {n : ℕ} (b : Fin n) :
Finset.image val (Finset.Iio b) = Finset.Iio ↑b

Finset.map along Fin.valEmbedding #

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 : ℕ} (a : Fin n) :
Finset.map valEmbedding (Finset.Iic a) = Finset.Iic ↑a
source
@[simp]
theorem Fin.map_valEmbedding_Iio {n : ℕ} (a : Fin n) :
Finset.map valEmbedding (Finset.Iio a) = Finset.Iio ↑a

Image under Fin.castLE #

source
@[simp]
theorem Fin.finsetImage_castLE_Icc {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.Icc a b) = Finset.Icc (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.finsetImage_castLE_Ico {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.Ico a b) = Finset.Ico (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.finsetImage_castLE_Ioc {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.Ioc a b) = Finset.Ioc (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.finsetImage_castLE_Ioo {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.Ioo a b) = Finset.Ioo (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.finsetImage_castLE_uIcc {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.uIcc a b) = Finset.uIcc (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.finsetImage_castLE_Iic {n m : ℕ} (a : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.Iic a) = Finset.Iic (castLE h a)
source
@[simp]
theorem Fin.finsetImage_castLE_Iio {n m : ℕ} (a : Fin n) (h : n ≤ m) :
Finset.image (castLE h) (Finset.Iio a) = Finset.Iio (castLE h a)

Finset.map along Fin.castLEEmb #

source
@[simp]
theorem Fin.map_castLEEmb_Icc {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.Icc a b) = Finset.Icc (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.map_castLEEmb_Ico {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.Ico a b) = Finset.Ico (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.map_castLEEmb_Ioc {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.Ioc a b) = Finset.Ioc (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.map_castLEEmb_Ioo {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.Ioo a b) = Finset.Ioo (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.map_castLEEmb_uIcc {n m : ℕ} (a b : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.uIcc a b) = Finset.uIcc (castLE h a) (castLE h b)
source
@[simp]
theorem Fin.map_castLEEmb_Iic {n m : ℕ} (a : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.Iic a) = Finset.Iic (castLE h a)
source
@[simp]
theorem Fin.map_castLEEmb_Iio {n m : ℕ} (a : Fin n) (h : n ≤ m) :
Finset.map (castLEEmb h) (Finset.Iio a) = Finset.Iio (castLE h a)

Images under Fin.castAdd #

source
@[simp]
theorem Fin.finsetImage_castAdd_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (castAdd m) (Finset.Icc i j) = Finset.Icc (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.finsetImage_castAdd_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (castAdd m) (Finset.Ico i j) = Finset.Ico (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.finsetImage_castAdd_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (castAdd m) (Finset.Ioc i j) = Finset.Ioc (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.finsetImage_castAdd_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (castAdd m) (Finset.Ioo i j) = Finset.Ioo (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.finsetImage_castAdd_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (castAdd m) (Finset.uIcc i j) = Finset.uIcc (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.finsetImage_castAdd_Ici {n : ℕ} (m : ℕ) [NeZero m] (i : Fin n) :
Finset.image (castAdd m) (Finset.Ici i) = Finset.Ico (castAdd m i) (natAdd n 0)
source
@[simp]
theorem Fin.finsetImage_castAdd_Ioi {n : ℕ} (m : ℕ) [NeZero m] (i : Fin n) :
Finset.image (castAdd m) (Finset.Ioi i) = Finset.Ioo (castAdd m i) (natAdd n 0)
source
@[simp]
theorem Fin.finsetImage_castAdd_Iic {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.image (castAdd m) (Finset.Iic i) = Finset.Iic (castAdd m i)
source
@[simp]
theorem Fin.finsetImage_castAdd_Iio {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.image (castAdd m) (Finset.Iio i) = Finset.Iio (castAdd m i)

Finset.map along Fin.castAddEmb #

source
@[simp]
theorem Fin.map_castAddEmb_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (castAddEmb m) (Finset.Icc i j) = Finset.Icc ((castAddEmb m) i) ((castAddEmb m) j)
source
@[simp]
theorem Fin.map_castAddEmb_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (castAddEmb m) (Finset.Ico i j) = Finset.Ico ((castAddEmb m) i) ((castAddEmb m) j)
source
@[simp]
theorem Fin.map_castAddEmb_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (castAddEmb m) (Finset.Ioc i j) = Finset.Ioc ((castAddEmb m) i) ((castAddEmb m) j)
source
@[simp]
theorem Fin.map_castAddEmb_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (castAddEmb m) (Finset.Ioo i j) = Finset.Ioo ((castAddEmb m) i) ((castAddEmb m) j)
source
@[simp]
theorem Fin.map_castAddEmb_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (castAddEmb m) (Finset.uIcc i j) = Finset.uIcc ((castAddEmb m) i) ((castAddEmb m) j)
source
@[simp]
theorem Fin.map_castAddEmb_Ici {n : ℕ} (m : ℕ) [NeZero m] (i : Fin n) :
Finset.map (castAddEmb m) (Finset.Ici i) = Finset.Ico ((castAddEmb m) i) (natAdd n 0)
source
@[simp]
theorem Fin.map_castAddEmb_Ioi {n : ℕ} (m : ℕ) [NeZero m] (i : Fin n) :
Finset.map (castAddEmb m) (Finset.Ioi i) = Finset.Ioo ((castAddEmb m) i) (natAdd n 0)
source
@[simp]
theorem Fin.map_castAddEmb_Iic {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.map (castAddEmb m) (Finset.Iic i) = Finset.Iic ((castAddEmb m) i)
source
@[simp]
theorem Fin.map_castAddEmb_Iio {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.map (castAddEmb m) (Finset.Iio i) = Finset.Iio ((castAddEmb m) i)

Images under Fin.cast #

source
@[simp]
theorem Fin.finsetImage_cast_Icc {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.image (Fin.cast h) (Finset.Icc i j) = Finset.Icc (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.finsetImage_cast_Ico {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.image (Fin.cast h) (Finset.Ico i j) = Finset.Ico (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.finsetImage_cast_Ioc {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.image (Fin.cast h) (Finset.Ioc i j) = Finset.Ioc (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.finsetImage_cast_Ioo {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.image (Fin.cast h) (Finset.Ioo i j) = Finset.Ioo (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.finsetImage_cast_uIcc {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.image (Fin.cast h) (Finset.uIcc i j) = Finset.uIcc (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.finsetImage_cast_Ici {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.image (Fin.cast h) (Finset.Ici i) = Finset.Ici (Fin.cast h i)
source
@[simp]
theorem Fin.finsetImage_cast_Ioi {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.image (Fin.cast h) (Finset.Ioi i) = Finset.Ioi (Fin.cast h i)
source
@[simp]
theorem Fin.finsetImage_cast_Iic {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.image (Fin.cast h) (Finset.Iic i) = Finset.Iic (Fin.cast h i)
source
@[simp]
theorem Fin.finsetImage_cast_Iio {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.image (Fin.cast h) (Finset.Iio i) = Finset.Iio (Fin.cast h i)

Finset.map along finCongr #

source
@[simp]
theorem Fin.map_finCongr_Icc {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Icc i j) = Finset.Icc (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.map_finCongr_Ico {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Ico i j) = Finset.Ico (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.map_finCongr_Ioc {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Ioc i j) = Finset.Ioc (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.map_finCongr_Ioo {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Ioo i j) = Finset.Ioo (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.map_finCongr_uIcc {n m : ℕ} (h : n = m) (i j : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.uIcc i j) = Finset.uIcc (Fin.cast h i) (Fin.cast h j)
source
@[simp]
theorem Fin.map_finCongr_Ici {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Ici i) = Finset.Ici (Fin.cast h i)
source
@[simp]
theorem Fin.map_finCongr_Ioi {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Ioi i) = Finset.Ioi (Fin.cast h i)
source
@[simp]
theorem Fin.map_finCongr_Iic {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Iic i) = Finset.Iic (Fin.cast h i)
source
@[simp]
theorem Fin.map_finCongr_Iio {n m : ℕ} (h : n = m) (i : Fin n) :
Finset.map (finCongr h).toEmbedding (Finset.Iio i) = Finset.Iio (Fin.cast h i)

Images under Fin.castSucc #

source
@[simp]
theorem Fin.finsetImage_castSucc_Icc {n : ℕ} (i j : Fin n) :
Finset.image castSucc (Finset.Icc i j) = Finset.Icc i.castSucc j.castSucc
source
@[simp]
theorem Fin.finsetImage_castSucc_Ico {n : ℕ} (i j : Fin n) :
Finset.image castSucc (Finset.Ico i j) = Finset.Ico i.castSucc j.castSucc
source
@[simp]
theorem Fin.finsetImage_castSucc_Ioc {n : ℕ} (i j : Fin n) :
Finset.image castSucc (Finset.Ioc i j) = Finset.Ioc i.castSucc j.castSucc
source
@[simp]
theorem Fin.finsetImage_castSucc_Ioo {n : ℕ} (i j : Fin n) :
Finset.image castSucc (Finset.Ioo i j) = Finset.Ioo i.castSucc j.castSucc
source
@[simp]
theorem Fin.finsetImage_castSucc_uIcc {n : ℕ} (i j : Fin n) :
Finset.image castSucc (Finset.uIcc i j) = Finset.uIcc i.castSucc j.castSucc
source
@[simp]
theorem Fin.finsetImage_castSucc_Ici {n : ℕ} (i : Fin n) :
Finset.image castSucc (Finset.Ici i) = Finset.Ico i.castSucc (last n)
source
@[simp]
theorem Fin.finsetImage_castSucc_Ioi {n : ℕ} (i : Fin n) :
Finset.image castSucc (Finset.Ioi i) = Finset.Ioo i.castSucc (last n)
source
@[simp]
theorem Fin.finsetImage_castSucc_Iic {n : ℕ} (i : Fin n) :
Finset.image castSucc (Finset.Iic i) = Finset.Iic i.castSucc
source
@[simp]
theorem Fin.finsetImage_castSucc_Iio {n : ℕ} (i : Fin n) :
Finset.image castSucc (Finset.Iio i) = Finset.Iio i.castSucc

Finset.map along Fin.castSuccEmb #

source
@[simp]
theorem Fin.map_castSuccEmb_Icc {n : ℕ} (i j : Fin n) :
Finset.map castSuccEmb (Finset.Icc i j) = Finset.Icc i.castSucc j.castSucc
source
@[simp]
theorem Fin.map_castSuccEmb_Ico {n : ℕ} (i j : Fin n) :
Finset.map castSuccEmb (Finset.Ico i j) = Finset.Ico i.castSucc j.castSucc
source
@[simp]
theorem Fin.map_castSuccEmb_Ioc {n : ℕ} (i j : Fin n) :
Finset.map castSuccEmb (Finset.Ioc i j) = Finset.Ioc i.castSucc j.castSucc
source
@[simp]
theorem Fin.map_castSuccEmb_Ioo {n : ℕ} (i j : Fin n) :
Finset.map castSuccEmb (Finset.Ioo i j) = Finset.Ioo i.castSucc j.castSucc
source
@[simp]
theorem Fin.map_castSuccEmb_uIcc {n : ℕ} (i j : Fin n) :
Finset.map castSuccEmb (Finset.uIcc i j) = Finset.uIcc i.castSucc j.castSucc
source
@[simp]
theorem Fin.map_castSuccEmb_Ici {n : ℕ} (i : Fin n) :
Finset.map castSuccEmb (Finset.Ici i) = Finset.Ico i.castSucc (last n)
source
@[simp]
theorem Fin.map_castSuccEmb_Ioi {n : ℕ} (i : Fin n) :
Finset.map castSuccEmb (Finset.Ioi i) = Finset.Ioo i.castSucc (last n)
source
@[simp]
theorem Fin.map_castSuccEmb_Iic {n : ℕ} (i : Fin n) :
Finset.map castSuccEmb (Finset.Iic i) = Finset.Iic i.castSucc
source
@[simp]
theorem Fin.map_castSuccEmb_Iio {n : ℕ} (i : Fin n) :
Finset.map castSuccEmb (Finset.Iio i) = Finset.Iio i.castSucc

Images under Fin.natAdd #

source
@[simp]
theorem Fin.finsetImage_natAdd_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (natAdd m) (Finset.Icc i j) = Finset.Icc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.finsetImage_natAdd_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (natAdd m) (Finset.Ico i j) = Finset.Ico (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.finsetImage_natAdd_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (natAdd m) (Finset.Ioc i j) = Finset.Ioc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.finsetImage_natAdd_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (natAdd m) (Finset.Ioo i j) = Finset.Ioo (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.finsetImage_natAdd_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (natAdd m) (Finset.uIcc i j) = Finset.uIcc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.finsetImage_natAdd_Ici {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.image (natAdd m) (Finset.Ici i) = Finset.Ici (natAdd m i)
source
@[simp]
theorem Fin.finsetImage_natAdd_Ioi {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.image (natAdd m) (Finset.Ioi i) = Finset.Ioi (natAdd m i)

Finset.map along Fin.natAddEmb #

source
@[simp]
theorem Fin.map_natAddEmb_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (natAddEmb m) (Finset.Icc i j) = Finset.Icc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.map_natAddEmb_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (natAddEmb m) (Finset.Ico i j) = Finset.Ico (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.map_natAddEmb_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (natAddEmb m) (Finset.Ioc i j) = Finset.Ioc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.map_natAddEmb_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (natAddEmb m) (Finset.Ioo i j) = Finset.Ioo (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.map_natAddEmb_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (natAddEmb m) (Finset.uIcc i j) = Finset.uIcc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.map_natAddEmb_Ici {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.map (natAddEmb m) (Finset.Ici i) = Finset.Ici (natAdd m i)
source
@[simp]
theorem Fin.map_natAddEmb_Ioi {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.map (natAddEmb m) (Finset.Ioi i) = Finset.Ioi (natAdd m i)

Images under Fin.addNat #

source
@[simp]
theorem Fin.finsetImage_addNat_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.Icc i j) = Finset.Icc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.finsetImage_addNat_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.Ico i j) = Finset.Ico (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.finsetImage_addNat_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.Ioc i j) = Finset.Ioc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.finsetImage_addNat_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.Ioo i j) = Finset.Ioo (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.finsetImage_addNat_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.uIcc i j) = Finset.uIcc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.finsetImage_addNat_Ici {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.Ici i) = Finset.Ici (i.addNat m)
source
@[simp]
theorem Fin.finsetImage_addNat_Ioi {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.image (fun (x : Fin n) => x.addNat m) (Finset.Ioi i) = Finset.Ioi (i.addNat m)

Finset.map along Fin.addNatEmb #

source
@[simp]
theorem Fin.map_addNatEmb_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (addNatEmb m) (Finset.Icc i j) = Finset.Icc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.map_addNatEmb_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (addNatEmb m) (Finset.Ico i j) = Finset.Ico (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.map_addNatEmb_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (addNatEmb m) (Finset.Ioc i j) = Finset.Ioc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.map_addNatEmb_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (addNatEmb m) (Finset.Ioo i j) = Finset.Ioo (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.map_addNatEmb_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
Finset.map (addNatEmb m) (Finset.uIcc i j) = Finset.uIcc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.map_addNatEmb_Ici {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.map (addNatEmb m) (Finset.Ici i) = Finset.Ici (i.addNat m)
source
@[simp]
theorem Fin.map_addNatEmb_Ioi {n : ℕ} (m : ℕ) (i : Fin n) :
Finset.map (addNatEmb m) (Finset.Ioi i) = Finset.Ioi (i.addNat m)

Images under Fin.succ #

source
@[simp]
theorem Fin.finsetImage_succ_Icc {n : ℕ} (i j : Fin n) :
Finset.image succ (Finset.Icc i j) = Finset.Icc i.succ j.succ
source
@[simp]
theorem Fin.finsetImage_succ_Ico {n : ℕ} (i j : Fin n) :
Finset.image succ (Finset.Ico i j) = Finset.Ico i.succ j.succ
source
@[simp]
theorem Fin.finsetImage_succ_Ioc {n : ℕ} (i j : Fin n) :
Finset.image succ (Finset.Ioc i j) = Finset.Ioc i.succ j.succ
source
@[simp]
theorem Fin.finsetImage_succ_Ioo {n : ℕ} (i j : Fin n) :
Finset.image succ (Finset.Ioo i j) = Finset.Ioo i.succ j.succ
source
@[simp]
theorem Fin.finsetImage_succ_uIcc {n : ℕ} (i j : Fin n) :
Finset.image succ (Finset.uIcc i j) = Finset.uIcc i.succ j.succ
source
@[simp]
theorem Fin.finsetImage_succ_Ici {n : ℕ} (i : Fin n) :
Finset.image succ (Finset.Ici i) = Finset.Ici i.succ
source
@[simp]
theorem Fin.finsetImage_succ_Ioi {n : ℕ} (i : Fin n) :
Finset.image succ (Finset.Ioi i) = Finset.Ioi i.succ
source
@[simp]
theorem Fin.finsetImage_succ_Iic {n : ℕ} (i : Fin n) :
Finset.image succ (Finset.Iic i) = Finset.Ioc 0 i.succ
source
@[simp]
theorem Fin.finsetImage_succ_Iio {n : ℕ} (i : Fin n) :
Finset.image succ (Finset.Iio i) = Finset.Ioo 0 i.succ

Finset.map along Fin.succEmb #

source
@[simp]
theorem Fin.map_succEmb_Icc {n : ℕ} (i j : Fin n) :
Finset.map (succEmb n) (Finset.Icc i j) = Finset.Icc i.succ j.succ
source
@[simp]
theorem Fin.map_succEmb_Ico {n : ℕ} (i j : Fin n) :
Finset.map (succEmb n) (Finset.Ico i j) = Finset.Ico i.succ j.succ
source
@[simp]
theorem Fin.map_succEmb_Ioc {n : ℕ} (i j : Fin n) :
Finset.map (succEmb n) (Finset.Ioc i j) = Finset.Ioc i.succ j.succ
source
@[simp]
theorem Fin.map_succEmb_Ioo {n : ℕ} (i j : Fin n) :
Finset.map (succEmb n) (Finset.Ioo i j) = Finset.Ioo i.succ j.succ
source
@[simp]
theorem Fin.map_succEmb_uIcc {n : ℕ} (i j : Fin n) :
Finset.map (succEmb n) (Finset.uIcc i j) = Finset.uIcc i.succ j.succ
source
@[simp]
theorem Fin.map_succEmb_Ici {n : ℕ} (i : Fin n) :
Finset.map (succEmb n) (Finset.Ici i) = Finset.Ici i.succ
source
@[simp]
theorem Fin.map_succEmb_Ioi {n : ℕ} (i : Fin n) :
Finset.map (succEmb n) (Finset.Ioi i) = Finset.Ioi i.succ
source
@[simp]
theorem Fin.map_succEmb_Iic {n : ℕ} (i : Fin n) :
Finset.map (succEmb n) (Finset.Iic i) = Finset.Ioc 0 i.succ
source
@[simp]
theorem Fin.map_succEmb_Iio {n : ℕ} (i : Fin n) :
Finset.map (succEmb n) (Finset.Iio i) = Finset.Ioo 0 i.succ

Images under Fin.rev #

source
@[simp]
theorem Fin.finsetImage_rev_Icc {n : ℕ} (i j : Fin n) :
Finset.image rev (Finset.Icc i j) = Finset.Icc j.rev i.rev
source
@[simp]
theorem Fin.finsetImage_rev_Ico {n : ℕ} (i j : Fin n) :
Finset.image rev (Finset.Ico i j) = Finset.Ioc j.rev i.rev
source
@[simp]
theorem Fin.finsetImage_rev_Ioc {n : ℕ} (i j : Fin n) :
Finset.image rev (Finset.Ioc i j) = Finset.Ico j.rev i.rev
source
@[simp]
theorem Fin.finsetImage_rev_Ioo {n : ℕ} (i j : Fin n) :
Finset.image rev (Finset.Ioo i j) = Finset.Ioo j.rev i.rev
source
@[simp]
theorem Fin.finsetImage_rev_uIcc {n : ℕ} (i j : Fin n) :
Finset.image rev (Finset.uIcc i j) = Finset.uIcc i.rev j.rev
source
@[simp]
theorem Fin.finsetImage_rev_Ici {n : ℕ} (i : Fin n) :
Finset.image rev (Finset.Ici i) = Finset.Iic i.rev
source
@[simp]
theorem Fin.finsetImage_rev_Ioi {n : ℕ} (i : Fin n) :
Finset.image rev (Finset.Ioi i) = Finset.Iio i.rev
source
@[simp]
theorem Fin.finsetImage_rev_Iic {n : ℕ} (i : Fin n) :
Finset.image rev (Finset.Iic i) = Finset.Ici i.rev
source
@[simp]
theorem Fin.finsetImage_rev_Iio {n : ℕ} (i : Fin n) :
Finset.image rev (Finset.Iio i) = Finset.Ioi i.rev

Finset.map along revPerm #

source
@[simp]
theorem Fin.map_revPerm_Icc {n : ℕ} (i j : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Icc i j) = Finset.Icc j.rev i.rev
source
@[simp]
theorem Fin.map_revPerm_Ico {n : ℕ} (i j : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Ico i j) = Finset.Ioc j.rev i.rev
source
@[simp]
theorem Fin.map_revPerm_Ioc {n : ℕ} (i j : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Ioc i j) = Finset.Ico j.rev i.rev
source
@[simp]
theorem Fin.map_revPerm_Ioo {n : ℕ} (i j : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Ioo i j) = Finset.Ioo j.rev i.rev
source
@[simp]
theorem Fin.map_revPerm_uIcc {n : ℕ} (i j : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.uIcc i j) = Finset.uIcc i.rev j.rev
source
@[simp]
theorem Fin.map_revPerm_Ici {n : ℕ} (i : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Ici i) = Finset.Iic i.rev
source
@[simp]
theorem Fin.map_revPerm_Ioi {n : ℕ} (i : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Ioi i) = Finset.Iio i.rev
source
@[simp]
theorem Fin.map_revPerm_Iic {n : ℕ} (i : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Iic i) = Finset.Ici i.rev
source
@[simp]
theorem Fin.map_revPerm_Iio {n : ℕ} (i : Fin n) :
Finset.map (Equiv.toEmbedding revPerm) (Finset.Iio i) = Finset.Ioi i.rev

Cardinalities of the intervals #

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