finsetImage_castAdd_Ioi — Mathlib

English

For any Fin n and m, with NeZero m, the image of the open interval Ioi i under castAddEmb m is Ioo (castAdd m i) (natAdd n 0).

Русский

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

LaTeX

$$$ (\mathrm{Finset}.Ioi\, i).image (\mathrm{Fin.castAddEmb}\, m) = \mathrm{Finset}.Ioo\ (\mathrm{Fin.castAdd}\, m\, i) (\mathrm{Fin.natAdd}\, n\, 0) $$$

Lean4

@[simp]
theorem finsetImage_castAdd_Ioi (m) [NeZero m] (i : Fin n) :
    (Ioi i).image (castAdd m) = Ioo (castAdd m i) (natAdd n 0) := by simp [← coe_inj]

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