orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb

English

The order-embedding of the complement of a singleton equals succAboveOrderEmb.

Русский

Встроенное отображение комплемента одинокого элемента равняется succAboveOrderEmb.

LaTeX

$$orderEmbOfFin_compl_singleton = Fin.succAboveOrderEmb$$

Lean4

@[simp]
theorem orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb {n : ℕ} (i : Fin (n + 1)) :
    ({ i }ᶜ : Finset _).orderEmbOfFin (by simp [card_compl]) = Fin.succAboveOrderEmb i :=
  orderEmbOfFin_compl_singleton _

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