preimage_rev_Iic — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\mathrm{rev}^{-1}(\\Iic i) = \\Ici(i^{\\mathrm{rev}}). $$$$

Lean4

@[simp]
theorem preimage_rev_Iic (i : Fin n) : rev ⁻¹' Iic i = Ici i.rev := by ext; simp [rev_le_iff]

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