preimage_castAdd_Ici_castAdd — Mathlib

English

For all m,n and i ∈ Fin n, the preimage of the interval [castAdd m i, ∞) under castAdd m is exactly [i, ∞).

Русский

Для всех m,n и i ∈ Fin n, предобраз отрезка [castAdd m i, ∞) под castAdd m совпадает с [i, ∞).

LaTeX

$$$$\\bigl(\\mathrm{Fin.castAdd}\\, m\\bigr)^{-1}\\bigl(\\mathrm{Ici}(\\mathrm{Fin.castAdd}\\, m\\, i)\\bigr) = \\mathrm{Ici}\\, i,$$$$

Lean4

@[simp]
theorem preimage_castAdd_Ici_castAdd (m) (i : Fin n) : castAdd m ⁻¹' Ici (castAdd m i) = Ici i :=
  rfl

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