castOrderEmbedding — Mathlib

English

There exists an order embedding from ℚ≥0 into K given by the usual embedding x ↦ x in K; this embedding preserves order and is injective.

Русский

Существует отображение, сохраняющее порядок, из ℚ≥0 в K, задаваемое обычным включением x ↦ x; оно инъективно и сохраняет порядок.

LaTeX

$$$\text{castOrderEmbedding} : \mathbb{Q}_{\ge 0} \hookrightarrow K$$$

Lean4

/-- Coercion from `ℚ` as an order embedding. -/
@[simps!]
def castOrderEmbedding : ℚ≥0 ↪o K :=
  OrderEmbedding.ofStrictMono (↑) cast_strictMono

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