toOrderEmbedding — Mathlib

English

An initial segment embedding between the < relations of two partial orders is an order embedding.

Русский

Начальное отрезковое отображение между отношениями ‹‰› двух частичных порядков является вложением порядка.

LaTeX

$$$\\\\text{toOrderEmbedding} \\\\bigl[f: r \\\\preccurlyeq_i s\\\\bigr] \\\\colon \\\\alpha \hookrightarrow \\\\beta$ is an order embedding.$$

Lean4

/-- An initial segment embedding between the `<` relations of two partial orders is an order
embedding. -/
def toOrderEmbedding [PartialOrder α] [PartialOrder β] (f : α ≤i β) : α ↪o β :=
  f.orderEmbeddingOfLTEmbedding

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