image_castAdd_Ioi — Mathlib

English

The image of the open ray Ioi i under Fin.castAdd m equals the open-closed interval Ioo (castAdd m i) (natAdd n 0).

Русский

Изображение луча Ioi i под Fin.castAdd m равно интервалу Ioo (castAdd m i) (natAdd n 0).

LaTeX

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

Lean4

@[simp]
theorem image_castAdd_Ioi (m) [NeZero m] (i : Fin n) : castAdd m '' Ioi i = Ioo (castAdd m i) (natAdd n 0) :=
  val_injective.image_injective <| by simp [← image_comp]

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