coeOrderHom — Mathlib

English

The embedding α ↪o WithBot α is an order embedding.

Русский

Вложение α → WithBot α является порядковым вложением.

LaTeX

$$$\\text{OrderEmbedding}(α \\rightarrow WithBot α)$$$

Lean4

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

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