finsetImage_castAdd_Ici — Mathlib

English

For any Fin n and natural m>0 with NeZero m, the image of the infinite interval Ici i under castAdd m equals the half-open interval Ico (castAdd m i) (natAdd n 0).

Русский

При любом i ∈ Fin n и m>0 (NeZero m) образ Ici i под castAdd m равен Ico (castAdd m i) (natAdd n 0).

LaTeX

$$$ (\mathrm{Finset}.Ici\, i).image (\mathrm{Fin.castAdd}\, m) = \mathrm{Finset}.Ico\ (\mathrm{Fin.castAdd}\, m\, i) (\mathrm{Fin.natAdd}\, n\, 0) $$$

Lean4

@[simp]
theorem finsetImage_castAdd_Ici (m) [NeZero m] (i : Fin n) :
    (Ici i).image (castAdd m) = Ico (castAdd m i) (natAdd n 0) := by simp [← coe_inj]

Похожие утверждения