English
The function that sends p ∈ Fin(n+1) to the subtype { x ≠ p } with the successor above is an order isomorphism between Fin n and that subtype.
Русский
Изоморфизм порядка между Fin n и подтипом { x ≠ p } с отношением выше следующего элемента.
LaTeX
$$$\text{finSuccAboveOrderIso}(p) : Fin n \simeq_o { x: Fin (n+1) // x ≠ p }$$$
Lean4
/-- Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying
values are retained. This is the `OrderIso` version of `Fin.castLE`. -/
@[simps apply symm_apply]
def castLEOrderIso {n m : ℕ} (h : n ≤ m) : Fin n ≃o { i : Fin m // (i : ℕ) < n }
where
toFun i := ⟨Fin.castLE h i, by simp⟩
invFun i := ⟨i, i.prop⟩
left_inv _ := by simp
right_inv _ := by simp
map_rel_iff' := by simp [(strictMono_castLE h).le_iff_le]
