preimage_castAdd_Ioo_castAdd — Mathlib

English

For all m,n and i,j ∈ Fin n, the preimage of the open interval (castAdd m i, castAdd m j) under castAdd m is exactly (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{Ioo}(\\mathrm{Fin.castAdd}\\, m\\, i, \\mathrm{Fin.castAdd}\\, m\\, j)\\bigr) = \\mathrm{Ioo}\\, i\\, j.$$$$

Lean4

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

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