preimage_castAdd_Ioc_castAdd — Mathlib

English

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

Lean4

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

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