English
Let α be a partially ordered set and β a preorder. If a map f: α → β satisfies f(a) ≤ f(b) iff a ≤ b for all a, b ∈ α, then f is an order embedding of α into β.
Русский
Пусть α — частично упорядченное множество, β — предуровень. Если отображение f: α → β удовлетворяет f(a) ≤ f(b) ⇔ a ≤ b для всех a, b ∈ α, тогда f является вложением по порядку α в β.
LaTeX
$$$\forall a,b\in\alpha:\ f(a)\le f(b) \iff a\le b \quad\Rightarrow\quad f \text{ является вложением по порядку } \alpha \hookrightarrow_o \beta$$$
Lean4
/-- To define an order embedding from a partial order to a preorder it suffices to give a function
together with a proof that it satisfies `f a ≤ f b ↔ a ≤ b`.
-/
def ofMapLEIff {α β} [PartialOrder α] [Preorder β] (f : α → β) (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) : α ↪o β :=
RelEmbedding.ofMapRelIff f hf
