The order isomorphism Fin (n + 1) ≃o {i}ᶜ

Given i : Fin (n + 2), we show that Fin.succAboveOrderEmb induces an order isomorphism Fin (n + 1) ≃o ({i}ᶜ : Finset (Fin (n + 2))).

noncomputable def Fin.succAboveOrderIso {n : ℕ} (i : Fin (n + 2)) : Fin (n + 1) ≃o { x : Fin (n + 2) // x ∈ {i}ᶜ }

Given i : Fin (n + 2), this is the order isomorphism between Fin (n + 1) and the finite set {i}ᶜ.

Equations

• i.succAboveOrderIso = { toEquiv := Equiv.ofBijective (fun (a : Fin (n + 1)) => ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯, map_rel_iff' := ⋯ }