preimage_rev_Iio — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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