preimage_castAdd_Iic_castAdd — Mathlib

English

For all m,n and i ∈ Fin n, the preimage of the nonincreasing ray (−∞, 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{Iic}(\\mathrm{Fin.castAdd}\\, m\\, i)\\bigr) = \\mathrm{Iic}\\, i.$$$$

Lean4

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

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