map_revPerm_Iio — Mathlib

English

Let n ∈ ℕ and i ∈ Fin n. Then the image of the lower interval { x ∈ Fin n : x < i } under the order-reversing bijection on Fin n is exactly the upper interval { x ∈ Fin n : i.rev < x }.

Русский

Пусть n ∈ ℕ и i ∈ Fin n. Тогда образ нижнего промежутка { x ∈ Fin n : x < i } под отображением, обращающим порядок, равен верхнему промежутку { x ∈ Fin n : i.rev < x }.

LaTeX

$$$\mathrm{revPerm}\bigl(Iio(i)\bigr) = Ioi(i^{\mathrm{rev}}).$$$

Lean4

@[simp]
theorem map_revPerm_Iio (i : Fin n) : (Iio i).map revPerm.toEmbedding = Ioi i.rev := by simp [← coe_inj]

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