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]