Documentation

Mathlib.Order.Interval.Set.Fin

(Pre)images of set intervals under Fin operations #

In this file we prove basic lemmas about preimages and images of the intervals under the following operations:

(Pre)images under Fin.val #

source
@[simp]
theorem Fin.range_val {n : ℕ} :
Set.range val = Set.Iio n
source
@[simp]
theorem Fin.preimage_val_Ici_val {n : ℕ} (i : Fin n) :
val ⁻¹' Set.Ici ↑i = Set.Ici i
source
@[simp]
theorem Fin.preimage_val_Ioi_val {n : ℕ} (i : Fin n) :
val ⁻¹' Set.Ioi ↑i = Set.Ioi i
source
@[simp]
theorem Fin.preimage_val_Iic_val {n : ℕ} (i : Fin n) :
val ⁻¹' Set.Iic ↑i = Set.Iic i
source
@[simp]
theorem Fin.preimage_val_Iio_val {n : ℕ} (i : Fin n) :
val ⁻¹' Set.Iio ↑i = Set.Iio i
source
@[simp]
theorem Fin.preimage_val_Icc_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Set.Icc ↑i ↑j = Set.Icc i j
source
@[simp]
theorem Fin.preimage_val_Ico_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Set.Ico ↑i ↑j = Set.Ico i j
source
@[simp]
theorem Fin.preimage_val_Ioc_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Set.Ioc ↑i ↑j = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_val_Ioo_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Set.Ioo ↑i ↑j = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_val_uIcc_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Set.uIcc ↑i ↑j = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_val_uIoc_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Ι ↑i ↑j = Ι i j
source
@[simp]
theorem Fin.preimage_val_uIoo_val {n : ℕ} (i j : Fin n) :
val ⁻¹' Set.uIoo ↑i ↑j = Set.uIoo i j
source
@[simp]
theorem Fin.image_val_Ici {n : ℕ} (i : Fin n) :
val '' Set.Ici i = Set.Ico (↑i) n
source
@[simp]
theorem Fin.image_val_Iic {n : ℕ} (i : Fin n) :
val '' Set.Iic i = Set.Iic ↑i
source
@[simp]
theorem Fin.image_val_Ioi {n : ℕ} (i : Fin n) :
val '' Set.Ioi i = Set.Ioo (↑i) n
source
@[simp]
theorem Fin.image_val_Iio {n : ℕ} (i : Fin n) :
val '' Set.Iio i = Set.Iio ↑i
source
@[simp]
theorem Fin.image_val_Icc {n : ℕ} (i j : Fin n) :
val '' Set.Icc i j = Set.Icc ↑i ↑j
source
@[simp]
theorem Fin.image_val_Ico {n : ℕ} (i j : Fin n) :
val '' Set.Ico i j = Set.Ico ↑i ↑j
source
@[simp]
theorem Fin.image_val_Ioc {n : ℕ} (i j : Fin n) :
val '' Set.Ioc i j = Set.Ioc ↑i ↑j
source
@[simp]
theorem Fin.image_val_Ioo {n : ℕ} (i j : Fin n) :
val '' Set.Ioo i j = Set.Ioo ↑i ↑j
source
@[simp]
theorem Fin.image_val_uIcc {n : ℕ} (i j : Fin n) :
val '' Set.uIcc i j = Set.uIcc ↑i ↑j
source
@[simp]
theorem Fin.image_val_uIoc {n : ℕ} (i j : Fin n) :
val '' Ι i j = Ι ↑i ↑j
source
@[simp]
theorem Fin.image_val_uIoo {n : ℕ} (i j : Fin n) :
val '' Set.uIoo i j = Set.uIoo ↑i ↑j

Preimages under Fin.castLE #

source
@[simp]
theorem Fin.preimage_castLE_Ici_castLE {m n : ℕ} (i : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Ici (castLE h i) = Set.Ici i
source
@[simp]
theorem Fin.preimage_castLE_Ioi_castLE {m n : ℕ} (i : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Ioi (castLE h i) = Set.Ioi i
source
@[simp]
theorem Fin.preimage_castLE_Iic_castLE {m n : ℕ} (i : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Iic (castLE h i) = Set.Iic i
source
@[simp]
theorem Fin.preimage_castLE_Iio_castLE {m n : ℕ} (i : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Iio (castLE h i) = Set.Iio i
source
@[simp]
theorem Fin.preimage_castLE_Icc_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Icc (castLE h i) (castLE h j) = Set.Icc i j
source
@[simp]
theorem Fin.preimage_castLE_Ico_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Ico (castLE h i) (castLE h j) = Set.Ico i j
source
@[simp]
theorem Fin.preimage_castLE_Ioc_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Ioc (castLE h i) (castLE h j) = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_castLE_Ioo_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.Ioo (castLE h i) (castLE h j) = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_castLE_uIcc_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.uIcc (castLE h i) (castLE h j) = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_castLE_uIoc_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Ι (castLE h i) (castLE h j) = Ι i j
source
@[simp]
theorem Fin.preimage_castLE_uIoo_castLE {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' Set.uIoo (castLE h i) (castLE h j) = Set.uIoo i j
source
@[simp]
theorem Fin.image_castLE_Iic {m n : ℕ} (i : Fin m) (h : m ≤ n) :
castLE h '' Set.Iic i = Set.Iic (castLE h i)
source
@[simp]
theorem Fin.image_castLE_Iio {m n : ℕ} (i : Fin m) (h : m ≤ n) :
castLE h '' Set.Iio i = Set.Iio (castLE h i)
source
@[simp]
theorem Fin.image_castLE_Icc {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Set.Icc i j = Set.Icc (castLE h i) (castLE h j)
source
@[simp]
theorem Fin.image_castLE_Ico {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Set.Ico i j = Set.Ico (castLE h i) (castLE h j)
source
@[simp]
theorem Fin.image_castLE_Ioc {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Set.Ioc i j = Set.Ioc (castLE h i) (castLE h j)
source
@[simp]
theorem Fin.image_castLE_Ioo {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Set.Ioo i j = Set.Ioo (castLE h i) (castLE h j)
source
@[simp]
theorem Fin.image_castLE_uIcc {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Set.uIcc i j = Set.uIcc (castLE h i) (castLE h j)
source
@[simp]
theorem Fin.image_castLE_uIoc {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Ι i j = Ι (castLE h i) (castLE h j)
source
@[simp]
theorem Fin.image_castLE_uIoo {m n : ℕ} (i j : Fin m) (h : m ≤ n) :
castLE h '' Set.uIoo i j = Set.uIoo (castLE h i) (castLE h j)

(Pre)images under Fin.castAdd #

source
@[simp]
theorem Fin.range_castAdd {m n : ℕ} [NeZero m] :
Set.range (castAdd m) = Set.Iio (natAdd n 0)
source
@[simp]
theorem Fin.preimage_castAdd_Ici_castAdd {n : ℕ} (m : ℕ) (i : Fin n) :
castAdd m ⁻¹' Set.Ici (castAdd m i) = Set.Ici i
source
@[simp]
theorem Fin.preimage_castAdd_Ioi_castAdd {n : ℕ} (m : ℕ) (i : Fin n) :
castAdd m ⁻¹' Set.Ioi (castAdd m i) = Set.Ioi i
source
@[simp]
theorem Fin.preimage_castAdd_Iic_castAdd {n : ℕ} (m : ℕ) (i : Fin n) :
castAdd m ⁻¹' Set.Iic (castAdd m i) = Set.Iic i
source
@[simp]
theorem Fin.preimage_castAdd_Iio_castAdd {n : ℕ} (m : ℕ) (i : Fin n) :
castAdd m ⁻¹' Set.Iio (castAdd m i) = Set.Iio i
source
@[simp]
theorem Fin.preimage_castAdd_Icc_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Set.Icc (castAdd m i) (castAdd m j) = Set.Icc i j
source
@[simp]
theorem Fin.preimage_castAdd_Ico_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Set.Ico (castAdd m i) (castAdd m j) = Set.Ico i j
source
@[simp]
theorem Fin.preimage_castAdd_Ioc_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Set.Ioc (castAdd m i) (castAdd m j) = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_castAdd_Ioo_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Set.Ioo (castAdd m i) (castAdd m j) = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_castAdd_uIcc_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Set.uIcc (castAdd m i) (castAdd m j) = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_castAdd_uIoc_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Ι (castAdd m i) (castAdd m j) = Ι i j
source
@[simp]
theorem Fin.preimage_castAdd_uIoo_castAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m ⁻¹' Set.uIoo (castAdd m i) (castAdd m j) = Set.uIoo i j
source
@[simp]
theorem Fin.image_castAdd_Ici {n : ℕ} (m : ℕ) [NeZero m] (i : Fin n) :
castAdd m '' Set.Ici i = Set.Ico (castAdd m i) (natAdd n 0)
source
@[simp]
theorem Fin.image_castAdd_Ioi {n : ℕ} (m : ℕ) [NeZero m] (i : Fin n) :
castAdd m '' Set.Ioi i = Set.Ioo (castAdd m i) (natAdd n 0)
source
@[simp]
theorem Fin.image_castAdd_Iic {n : ℕ} (m : ℕ) (i : Fin n) :
castAdd m '' Set.Iic i = Set.Iic (castAdd m i)
source
@[simp]
theorem Fin.image_castAdd_Iio {n : ℕ} (m : ℕ) (i : Fin n) :
castAdd m '' Set.Iio i = Set.Iio (castAdd m i)
source
@[simp]
theorem Fin.image_castAdd_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Set.Icc i j = Set.Icc (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.image_castAdd_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Set.Ico i j = Set.Ico (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.image_castAdd_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Set.Ioc i j = Set.Ioc (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.image_castAdd_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Set.Ioo i j = Set.Ioo (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.image_castAdd_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Set.uIcc i j = Set.uIcc (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.image_castAdd_uIoc {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Ι i j = Ι (castAdd m i) (castAdd m j)
source
@[simp]
theorem Fin.image_castAdd_uIoo {n : ℕ} (m : ℕ) (i j : Fin n) :
castAdd m '' Set.uIoo i j = Set.uIoo (castAdd m i) (castAdd m j)

(Pre)images under Fin.cast #

source
theorem Fin.image_cast {m n : ℕ} (h : m = n) (s : Set (Fin m)) :
Fin.cast h '' s = Fin.cast ⋯ ⁻¹' s
source
@[simp]
theorem Fin.image_cast_fun {m n : ℕ} (h : m = n) :
Set.image (Fin.cast h) = Set.preimage (Fin.cast ⋯)
source
@[simp]
theorem Fin.preimage_cast_Ici {m n : ℕ} (h : m = n) (i : Fin n) :
Fin.cast h ⁻¹' Set.Ici i = Set.Ici (Fin.cast ⋯ i)
source
@[simp]
theorem Fin.preimage_cast_Ioi {m n : ℕ} (h : m = n) (i : Fin n) :
Fin.cast h ⁻¹' Set.Ioi i = Set.Ioi (Fin.cast ⋯ i)
source
@[simp]
theorem Fin.preimage_cast_Iic {m n : ℕ} (h : m = n) (i : Fin n) :
Fin.cast h ⁻¹' Set.Iic i = Set.Iic (Fin.cast ⋯ i)
source
@[simp]
theorem Fin.preimage_cast_Iio {m n : ℕ} (h : m = n) (i : Fin n) :
Fin.cast h ⁻¹' Set.Iio i = Set.Iio (Fin.cast ⋯ i)
source
@[simp]
theorem Fin.preimage_cast_Icc {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Set.Icc i j = Set.Icc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
source
@[simp]
theorem Fin.preimage_cast_Ico {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Set.Ico i j = Set.Ico (Fin.cast ⋯ i) (Fin.cast ⋯ j)
source
@[simp]
theorem Fin.preimage_cast_Ioc {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Set.Ioc i j = Set.Ioc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
source
@[simp]
theorem Fin.preimage_cast_Ioo {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Set.Ioo i j = Set.Ioo (Fin.cast ⋯ i) (Fin.cast ⋯ j)
source
@[simp]
theorem Fin.preimage_cast_uIcc {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Set.uIcc i j = Set.uIcc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
source
@[simp]
theorem Fin.preimage_cast_uIoc {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Ι i j = Ι (Fin.cast ⋯ i) (Fin.cast ⋯ j)
source
@[simp]
theorem Fin.preimage_cast_uIoo {m n : ℕ} (h : m = n) (i j : Fin n) :
Fin.cast h ⁻¹' Set.uIoo i j = Set.uIoo (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Fin.castSucc #

source
@[simp]
theorem Fin.preimage_castSucc_Ici_castSucc {n : ℕ} (i : Fin n) :
castSucc ⁻¹' Set.Ici i.castSucc = Set.Ici i
source
@[simp]
theorem Fin.preimage_castSucc_Ioi_castSucc {n : ℕ} (i : Fin n) :
castSucc ⁻¹' Set.Ioi i.castSucc = Set.Ioi i
source
@[simp]
theorem Fin.preimage_castSucc_Iic_castSucc {n : ℕ} (i : Fin n) :
castSucc ⁻¹' Set.Iic i.castSucc = Set.Iic i
source
@[simp]
theorem Fin.preimage_castSucc_Iio_castSucc {n : ℕ} (i : Fin n) :
castSucc ⁻¹' Set.Iio i.castSucc = Set.Iio i
source
@[simp]
theorem Fin.preimage_castSucc_Icc_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Set.Icc i.castSucc j.castSucc = Set.Icc i j
source
@[simp]
theorem Fin.preimage_castSucc_Ico_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Set.Ico i.castSucc j.castSucc = Set.Ico i j
source
@[simp]
theorem Fin.preimage_castSucc_Ioc_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Set.Ioc i.castSucc j.castSucc = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_castSucc_Ioo_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Set.Ioo i.castSucc j.castSucc = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_castSucc_uIcc_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Set.uIcc i.castSucc j.castSucc = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_castSucc_uIoc_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Ι i.castSucc j.castSucc = Ι i j
source
@[simp]
theorem Fin.preimage_castSucc_uIoo_castSucc {n : ℕ} (i j : Fin n) :
castSucc ⁻¹' Set.uIoo i.castSucc j.castSucc = Set.uIoo i j
source
@[simp]
theorem Fin.image_castSucc_Ici {n : ℕ} (i : Fin n) :
castSucc '' Set.Ici i = Set.Ico i.castSucc (last n)
source
@[simp]
theorem Fin.image_castSucc_Ioi {n : ℕ} (i : Fin n) :
castSucc '' Set.Ioi i = Set.Ioo i.castSucc (last n)
source
@[simp]
theorem Fin.image_castSucc_Iic {n : ℕ} (i : Fin n) :
castSucc '' Set.Iic i = Set.Iic i.castSucc
source
@[simp]
theorem Fin.image_castSucc_Iio {n : ℕ} (i : Fin n) :
castSucc '' Set.Iio i = Set.Iio i.castSucc
source
@[simp]
theorem Fin.image_castSucc_Icc {n : ℕ} (i j : Fin n) :
castSucc '' Set.Icc i j = Set.Icc i.castSucc j.castSucc
source
@[simp]
theorem Fin.image_castSucc_Ico {n : ℕ} (i j : Fin n) :
castSucc '' Set.Ico i j = Set.Ico i.castSucc j.castSucc
source
@[simp]
theorem Fin.image_castSucc_Ioc {n : ℕ} (i j : Fin n) :
castSucc '' Set.Ioc i j = Set.Ioc i.castSucc j.castSucc
source
@[simp]
theorem Fin.image_castSucc_Ioo {n : ℕ} (i j : Fin n) :
castSucc '' Set.Ioo i j = Set.Ioo i.castSucc j.castSucc
source
@[simp]
theorem Fin.image_castSucc_uIcc {n : ℕ} (i j : Fin n) :
castSucc '' Set.uIcc i j = Set.uIcc i.castSucc j.castSucc
source
@[simp]
theorem Fin.image_castSucc_uIoc {n : ℕ} (i j : Fin n) :
castSucc '' Ι i j = Ι i.castSucc j.castSucc
source
@[simp]
theorem Fin.image_castSucc_uIoo {n : ℕ} (i j : Fin n) :
castSucc '' Set.uIoo i j = Set.uIoo i.castSucc j.castSucc

Fin.natAdd #

source
theorem Fin.range_natAdd (m n : ℕ) :
Set.range (natAdd m) = {i : Fin (m + n) | m ≤ ↑i}
source
theorem Fin.range_natAdd_eq_Ici (m n : ℕ) [NeZero n] :
Set.range (natAdd m) = Set.Ici (natAdd m 0)
source
theorem Fin.range_natAdd_eq_Ioi (m n : ℕ) [NeZero m] :
Set.range (natAdd m) = Set.Ioi (castAdd n ⊤)
source
@[simp]
theorem Fin.preimage_natAdd_Ici_natAdd {n : ℕ} (m : ℕ) (i : Fin n) :
natAdd m ⁻¹' Set.Ici (natAdd m i) = Set.Ici i
source
@[simp]
theorem Fin.preimage_natAdd_Ioi_natAdd {n : ℕ} (m : ℕ) (i : Fin n) :
natAdd m ⁻¹' Set.Ioi (natAdd m i) = Set.Ioi i
source
@[simp]
theorem Fin.preimage_natAdd_Iic_natAdd {n : ℕ} (m : ℕ) (i : Fin n) :
natAdd m ⁻¹' Set.Iic (natAdd m i) = Set.Iic i
source
@[simp]
theorem Fin.preimage_natAdd_Iio_natAdd {n : ℕ} (m : ℕ) (i : Fin n) :
natAdd m ⁻¹' Set.Iio (natAdd m i) = Set.Iio i
source
@[simp]
theorem Fin.preimage_natAdd_Icc_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Set.Icc (natAdd m i) (natAdd m j) = Set.Icc i j
source
@[simp]
theorem Fin.preimage_natAdd_Ico_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Set.Ico (natAdd m i) (natAdd m j) = Set.Ico i j
source
@[simp]
theorem Fin.preimage_natAdd_Ioc_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Set.Ioc (natAdd m i) (natAdd m j) = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_natAdd_Ioo_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Set.Ioo (natAdd m i) (natAdd m j) = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_natAdd_uIcc_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Set.uIcc (natAdd m i) (natAdd m j) = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_natAdd_uIoc_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Ι (natAdd m i) (natAdd m j) = Ι i j
source
@[simp]
theorem Fin.preimage_natAdd_uIoo_natAdd {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m ⁻¹' Set.uIoo (natAdd m i) (natAdd m j) = Set.uIoo i j
source
@[simp]
theorem Fin.image_natAdd_Ici {n : ℕ} (m : ℕ) (i : Fin n) :
natAdd m '' Set.Ici i = Set.Ici (natAdd m i)
source
@[simp]
theorem Fin.image_natAdd_Ioi {n : ℕ} (m : ℕ) (i : Fin n) :
natAdd m '' Set.Ioi i = Set.Ioi (natAdd m i)
source
@[simp]
theorem Fin.image_natAdd_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Set.Icc i j = Set.Icc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.image_natAdd_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Set.Ico i j = Set.Ico (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.image_natAdd_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Set.Ioc i j = Set.Ioc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.image_natAdd_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Set.Ioo i j = Set.Ioo (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.image_natAdd_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Set.uIcc i j = Set.uIcc (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.image_natAdd_uIoc {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Ι i j = Ι (natAdd m i) (natAdd m j)
source
@[simp]
theorem Fin.image_natAdd_uIoo {n : ℕ} (m : ℕ) (i j : Fin n) :
natAdd m '' Set.uIoo i j = Set.uIoo (natAdd m i) (natAdd m j)

Fin.addNat #

source
@[simp]
theorem Fin.preimage_addNat_Ici_addNat {n : ℕ} (m : ℕ) (i : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Ici (i.addNat m) = Set.Ici i
source
@[simp]
theorem Fin.preimage_addNat_Ioi_addNat {n : ℕ} (m : ℕ) (i : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Ioi (i.addNat m) = Set.Ioi i
source
@[simp]
theorem Fin.preimage_addNat_Iic_addNat {n : ℕ} (m : ℕ) (i : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Iic (i.addNat m) = Set.Iic i
source
@[simp]
theorem Fin.preimage_addNat_Iio_addNat {n : ℕ} (m : ℕ) (i : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Iio (i.addNat m) = Set.Iio i
source
@[simp]
theorem Fin.preimage_addNat_Icc_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Icc (i.addNat m) (j.addNat m) = Set.Icc i j
source
@[simp]
theorem Fin.preimage_addNat_Ico_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Ico (i.addNat m) (j.addNat m) = Set.Ico i j
source
@[simp]
theorem Fin.preimage_addNat_Ioc_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Ioc (i.addNat m) (j.addNat m) = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_addNat_Ioo_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.Ioo (i.addNat m) (j.addNat m) = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_addNat_uIcc_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.uIcc (i.addNat m) (j.addNat m) = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_addNat_uIoc_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Ι (i.addNat m) (j.addNat m) = Ι i j
source
@[simp]
theorem Fin.preimage_addNat_uIoo_addNat {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) ⁻¹' Set.uIoo (i.addNat m) (j.addNat m) = Set.uIoo i j
source
@[simp]
theorem Fin.image_addNat_Ici {n : ℕ} (m : ℕ) (i : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.Ici i = Set.Ici (i.addNat m)
source
@[simp]
theorem Fin.image_addNat_Ioi {n : ℕ} (m : ℕ) (i : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.Ioi i = Set.Ioi (i.addNat m)
source
@[simp]
theorem Fin.image_addNat_Icc {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.Icc i j = Set.Icc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.image_addNat_Ico {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.Ico i j = Set.Ico (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.image_addNat_Ioc {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.Ioc i j = Set.Ioc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.image_addNat_Ioo {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.Ioo i j = Set.Ioo (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.image_addNat_uIcc {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.uIcc i j = Set.uIcc (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.image_addNat_uIoc {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Ι i j = Ι (i.addNat m) (j.addNat m)
source
@[simp]
theorem Fin.image_addNat_uIoo {n : ℕ} (m : ℕ) (i j : Fin n) :
(fun (x : Fin n) => x.addNat m) '' Set.uIoo i j = Set.uIoo (i.addNat m) (j.addNat m)

Fin.succ #

source
@[simp]
theorem Fin.preimage_succ_Ici_succ {n : ℕ} (i : Fin n) :
succ ⁻¹' Set.Ici i.succ = Set.Ici i
source
@[simp]
theorem Fin.preimage_succ_Ioi_succ {n : ℕ} (i : Fin n) :
succ ⁻¹' Set.Ioi i.succ = Set.Ioi i
source
@[simp]
theorem Fin.preimage_succ_Iic_succ {n : ℕ} (i : Fin n) :
succ ⁻¹' Set.Iic i.succ = Set.Iic i
source
@[simp]
theorem Fin.preimage_succ_Iio_succ {n : ℕ} (i : Fin n) :
succ ⁻¹' Set.Iio i.succ = Set.Iio i
source
@[simp]
theorem Fin.preimage_succ_Icc_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Set.Icc i.succ j.succ = Set.Icc i j
source
@[simp]
theorem Fin.preimage_succ_Ico_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Set.Ico i.succ j.succ = Set.Ico i j
source
@[simp]
theorem Fin.preimage_succ_Ioc_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Set.Ioc i.succ j.succ = Set.Ioc i j
source
@[simp]
theorem Fin.preimage_succ_Ioo_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Set.Ioo i.succ j.succ = Set.Ioo i j
source
@[simp]
theorem Fin.preimage_succ_uIcc_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Set.uIcc i.succ j.succ = Set.uIcc i j
source
@[simp]
theorem Fin.preimage_succ_uIoc_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Ι i.succ j.succ = Ι i j
source
@[simp]
theorem Fin.preimage_succ_uIoo_succ {n : ℕ} (i j : Fin n) :
succ ⁻¹' Set.uIoo i.succ j.succ = Set.uIoo i j
source
@[simp]
theorem Fin.image_succ_Ici {n : ℕ} (i : Fin n) :
succ '' Set.Ici i = Set.Ici i.succ
source
@[simp]
theorem Fin.image_succ_Ioi {n : ℕ} (i : Fin n) :
succ '' Set.Ioi i = Set.Ioi i.succ
source
@[simp]
theorem Fin.image_succ_Iic {n : ℕ} (i : Fin n) :
succ '' Set.Iic i = Set.Ioc 0 i.succ
source
@[simp]
theorem Fin.image_succ_Iio {n : ℕ} (i : Fin n) :
succ '' Set.Iio i = Set.Ioo 0 i.succ
source
@[simp]
theorem Fin.image_succ_Icc {n : ℕ} (i j : Fin n) :
succ '' Set.Icc i j = Set.Icc i.succ j.succ
source
@[simp]
theorem Fin.image_succ_Ico {n : ℕ} (i j : Fin n) :
succ '' Set.Ico i j = Set.Ico i.succ j.succ
source
@[simp]
theorem Fin.image_succ_Ioc {n : ℕ} (i j : Fin n) :
succ '' Set.Ioc i j = Set.Ioc i.succ j.succ
source
@[simp]
theorem Fin.image_succ_Ioo {n : ℕ} (i j : Fin n) :
succ '' Set.Ioo i j = Set.Ioo i.succ j.succ
source
@[simp]
theorem Fin.image_succ_uIcc {n : ℕ} (i j : Fin n) :
succ '' Set.uIcc i j = Set.uIcc i.succ j.succ
source
@[simp]
theorem Fin.image_succ_uIoc {n : ℕ} (i j : Fin n) :
succ '' Ι i j = Ι i.succ j.succ
source
@[simp]
theorem Fin.image_succ_uIoo {n : ℕ} (i j : Fin n) :
succ '' Set.uIoo i j = Set.uIoo i.succ j.succ

Fin.rev #

source
@[simp]
theorem Fin.range_rev {n : ℕ} :
Set.range rev = Set.univ
source
theorem Fin.image_rev {n : ℕ} (s : Set (Fin n)) :
rev '' s = rev ⁻¹' s
source
@[simp]
theorem Fin.image_rev_fun {n : ℕ} :
Set.image rev = Set.preimage rev
source
@[simp]
theorem Fin.preimage_rev_Ici {n : ℕ} (i : Fin n) :
rev ⁻¹' Set.Ici i = Set.Iic i.rev
source
@[simp]
theorem Fin.preimage_rev_Ioi {n : ℕ} (i : Fin n) :
rev ⁻¹' Set.Ioi i = Set.Iio i.rev
source
@[simp]
theorem Fin.preimage_rev_Iic {n : ℕ} (i : Fin n) :
rev ⁻¹' Set.Iic i = Set.Ici i.rev
source
@[simp]
theorem Fin.preimage_rev_Iio {n : ℕ} (i : Fin n) :
rev ⁻¹' Set.Iio i = Set.Ioi i.rev
source
@[simp]
theorem Fin.preimage_rev_Icc {n : ℕ} (i j : Fin n) :
rev ⁻¹' Set.Icc i j = Set.Icc j.rev i.rev
source
@[simp]
theorem Fin.preimage_rev_Ico {n : ℕ} (i j : Fin n) :
rev ⁻¹' Set.Ico i j = Set.Ioc j.rev i.rev
source
@[simp]
theorem Fin.preimage_rev_Ioc {n : ℕ} (i j : Fin n) :
rev ⁻¹' Set.Ioc i j = Set.Ico j.rev i.rev
source
@[simp]
theorem Fin.preimage_rev_Ioo {n : ℕ} (i j : Fin n) :
rev ⁻¹' Set.Ioo i j = Set.Ioo j.rev i.rev
source
@[simp]
theorem Fin.preimage_rev_uIcc {n : ℕ} (i j : Fin n) :
rev ⁻¹' Set.uIcc i j = Set.uIcc i.rev j.rev
source
@[simp]
theorem Fin.preimage_rev_uIoo {n : ℕ} (i j : Fin n) :
rev ⁻¹' Set.uIoo i j = Set.uIoo i.rev j.rev