English
Embeddings of partial orders that preserve < also preserve ≤; i.e., from a LT-embedding between α and β, one constructs an OrderEmbedding α → β.
Русский
Вложение частичных порядков, сохраняющее <, также сохраняет ≤; из LT-вложения между α и β строится вложение α ↪o β.
LaTeX
$$$\\text{orderEmbeddingOfLTEmbedding} : [\\partial order\\ α] [\\partial order\\ β] \\rightarrow ((\\cdot < \\cdot) : α \\to α \\to \\mathrm{Prop}) \\\\hookrightarrow_r ((\\cdot < \\cdot) : β \\to β \\to \\mathrm{Prop}) \\rightarrow α \\hookrightarrow_o β.$$$
Lean4
/-- Embeddings of partial orders that preserve `<` also preserve `≤`. -/
def orderEmbeddingOfLTEmbedding [PartialOrder α] [PartialOrder β]
(f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) : α ↪o β :=
{ f with map_rel_iff' := by simp [le_iff_lt_or_eq, f.map_rel_iff, f.injective.eq_iff] }
