preimage_natAdd_Ioo_natAdd — Mathlib

English

For all m and i, j in Fin n, the preimage of Ioo(natAdd m i) (natAdd m j) under natAdd m is Ioo i j.

Русский

Для всех m и i, j ∈ Fin n, прообраз Ioo(natAdd m i, natAdd m j) под natAdd m равен Ioo i j.

LaTeX

$$$\operatorname{natAdd}(m)^{-1}(\mathrm{Ioo}(\mathrm{natAdd}(m,i), \mathrm{natAdd}(m,j))) = \mathrm{Ioo}(i, j)$$$

Lean4

@[simp]
theorem preimage_natAdd_Ioo_natAdd (m) (i j : Fin n) : natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) = Ioo i j := by ext;
  simp

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