English
Let p,q be predicates on α and h a function sending p-true elements to q-true elements. The natural inclusion map from {x : α | p x} to {x : α | q x} given by x ↦ ⟨x, h x (proof)⟩ is an order embedding.
Русский
Пусть p,q — предикаты на α и h: ∀a, p(a) → q(a). Натуральное вложение подтипа p в подтип q, отображающее ⟨a, proof_p⟩ в ⟨a, h(a, proof_p)⟩, является вложением по порядку.
LaTeX
$$$\\operatorname{Subtype.orderEmbedding}_{p,q,h} : \\{x:\\\\alpha \\\\mid p(x)\\} \\hookrightarrow_o \\\\{x:\\\\alpha \\\\mid q(x)\\}$.$$
Lean4
/-- `Subtype.impEmbedding` as an order embedding. -/
@[simps!]
def _root_.Subtype.orderEmbedding {p q : α → Prop} (h : ∀ a, p a → q a) : { x // p x } ↪o { x // q x } :=
{ Subtype.impEmbedding _ _ h with map_rel_iff' := by aesop }
