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]