preimage_rev_Ici — Mathlib

English

For every i ∈ Fin(n), the preimage under rev of the upper ray starting at i equals the lower ray ending at i.rev; i.e., rev^{-1}([i, ∞)) = {x : x ≤ i.rev}.

Русский

Для любого i ∈ Fin(n) прообраз разворота от верхнего полупрямого от i равен нижнему лучу, заканчивающемуся в i.rev; то есть rev^{-1}([i, ∞)) = {x ≤ i.rev}.

LaTeX

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

Lean4

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

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