English
The order embedding of the complement of a singleton {i} is the composition of a natural order isomorphism with succAboveOrderEmb.
Русский
Встроенное отображение комплемента одиночного множества {i} эквивалентно композиции естественного изоморфизма порядка и succAboveOrderEmb.
LaTeX
$$orderEmbOfFin_compl_singleton = (Fin.castOrderIso \; \text{...}).toOrderEmbedding.trans (Fin.succAboveOrderEmb i)$$
Lean4
theorem orderEmbOfFin_compl_singleton {n : ℕ} {i : Fin (n + 1)} {k : ℕ} (h : ({ i }ᶜ : Finset _).card = k) :
({ i }ᶜ : Finset _).orderEmbOfFin h =
(Fin.castOrderIso <| by simp_all [card_compl]).toOrderEmbedding.trans (Fin.succAboveOrderEmb i) :=
by
apply DFunLike.coe_injective
rw [eq_comm]
convert orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))
· simp
· simp [← h, card_compl]
