preimage_rev_Icc — Mathlib

English

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

Русский

Для i, j ∈ Fin(n) прообраз разворота от замкнутого интервала Icc i j равен Icc j.rev i.rev.

LaTeX

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

Lean4

@[simp]
theorem preimage_rev_Icc (i j : Fin n) : rev ⁻¹' Icc i j = Icc j.rev i.rev := by ext;
  simp [le_rev_iff, rev_le_iff, and_comm]

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