toOrderEmbedding — Mathlib

English

A RightOrdContinuous function f that is injective yields an order-embedding via the construction toOrderEmbedding.

Русский

Право-непрерывная инъективная функция обеспечивает вложение по порядку через конструкцию toOrderEmbedding.

LaTeX

$$$ (\\text{toOrderEmbedding}\\; f\\; h) : \\alpha \\hookrightarrow_o \\beta. $$$

Lean4

/-- Convert an injective left order continuous function to an `OrderEmbedding`. -/
def toOrderEmbedding (hf : RightOrdContinuous f) (h : Injective f) : α ↪o β :=
  ⟨⟨f, h⟩, hf.le_iff h⟩

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