preimage_rev_uIcc — Mathlib

English

For i, j ∈ Fin(n), the preimage under rev of the union-closed interval uIcc i j equals uIcc i.rev j.rev; i.e., rev^{-1}(uIcc(i,j)) = uIcc(i.rev, j.rev).

Русский

Для i, j ∈ Fin(n) прообраз разворота от uIcc i j равен uIcc(i.rev, j.rev).

LaTeX

$$$$ \\mathrm{rev}^{-1}(\\mathrm{uIcc}\\, i j) = \\mathrm{uIcc}\\,(i^{\\mathrm{rev}})\,(j^{\\mathrm{rev}}). $$$$

Lean4

@[simp]
theorem preimage_rev_uIcc (i j : Fin n) : rev ⁻¹' uIcc i j = uIcc i.rev j.rev := by
  simp [uIcc, ← rev_anti.map_min, ← rev_anti.map_max]

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