toLinearExtension — Mathlib

English

There is an order-preserving embedding from α into its linear extension LinearExtension α.

Русский

Существует порядок-произведение отображения из α в линейное расширение LinearExtension α.

LaTeX

$$$\exists e: α \to^{{\le}} LinearExtension α$$$

Lean4

/-- The embedding of `α` into `LinearExtension α` as an order homomorphism. -/
noncomputable def toLinearExtension {α : Type u} [PartialOrder α] : α →o LinearExtension α
    where
  toFun x := x
  monotone' := (extend_partialOrder ((· ≤ ·) : α → α → Prop)).choose_spec.2

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