coeOrderHom — Mathlib

English

The embedding a ↦ a defines an order embedding α ↪o WithTop α.

Русский

Отображение a ↦ a образует упорядочение как вложение α → WithTop α.

LaTeX

$$$\\text{OrderEmbedding}(a \\mapsto a) : α \\hookrightarrow\\mathrm{WithTop} α$$$

Lean4

/-- The coercion `α → WithTop α` bundled as monotone map. -/
@[simps -fullyApplied]
def coeOrderHom {α : Type*} [Preorder α] : α ↪o WithTop α
    where
  toFun := (↑)
  inj' := WithTop.coe_injective
  map_rel_iff' := WithTop.coe_le_coe

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