preimage_natAdd_uIoc_natAdd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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