preimage_castAdd_Icc_castAdd — Mathlib

English

For all m,n and i,j ∈ Fin n, the preimage of the closed interval [castAdd m i, castAdd m j] under castAdd m is exactly the closed interval [i, j].

Русский

Для всех m,n и i,j ∈ Fin n, предобраз [castAdd m i, castAdd m j] под castAdd m равен [i, j].

LaTeX

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

Lean4

@[simp]
theorem preimage_castAdd_Icc_castAdd (m) (i j : Fin n) : castAdd m ⁻¹' Icc (castAdd m i) (castAdd m j) = Icc i j :=
  rfl

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