preimage_natAdd_uIoo_natAdd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_natAdd_uIoo_natAdd (m) (i j : Fin n) : natAdd m ⁻¹' uIoo (natAdd m i) (natAdd m j) = uIoo i j := by
  simp [uIoo, ← (strictMono_natAdd m).monotone.map_max, ← (strictMono_natAdd m).monotone.map_min]

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