preimage_natAdd_uIcc_natAdd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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