preimage_rev_Ioi — Mathlib

English

For every i ∈ Fin(n), the preimage under rev of the open upper interval Ioi i equals the open lower interval Iio i.rev; i.e., rev^{-1}(Ioi(i)) = Iio(i.rev).

Русский

Для любого i ∈ Fin(n) прообраз разворота от открытого верхнего интервала Ioi i равен открытому нижнему интервалу Iio i.rev.

LaTeX

$$$$ \\mathrm{rev}^{-1}(\\Ioi i) = \\Iio(i^{\\mathrm{rev}}). $$$$

Lean4

@[simp]
theorem preimage_rev_Ioi (i : Fin n) : rev ⁻¹' Ioi i = Iio i.rev := by ext; simp [lt_rev_iff]

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