castOrderEmbedding — Mathlib

English

There is an order-preserving embedding of ℚ into any ordered field K.

Русский

Существует вложение ℚ в упорядоченное поле K, сохраняющее порядок.

LaTeX

$$$ \text{def castOrderEmbedding } : \mathbb{Q} \hookrightarrow_o K $ (as an order-embedding). $$$

Lean4

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

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