ofStrictMono — Mathlib

English

A strictly monotone map from a linear order into a preorder is an order embedding.

Русский

Строго монотонное отображение из линейного порядка в предуровень является вложением по порядку.

LaTeX

$$$\forall a,b\in\alpha:\ a\le b \iff f(a)\le f(b)$$

Lean4

/-- A strictly monotone map from a linear order is an order embedding. -/
def ofStrictMono {α β} [LinearOrder α] [Preorder β] (f : α → β) (h : StrictMono f) : α ↪o β :=
  ofMapLEIff f fun _ _ => h.le_iff_le

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