preimage_castAdd_Ico_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{Ico}(\\mathrm{Fin.castAdd}\\, m\\, i, \\mathrm{Fin.castAdd}\\, m\\, j)\\bigr) = \\mathrm{Ico}\\, i\\, j.$$$$

Lean4

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

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