preimage_rev_uIoo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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