English
Let α be a preorder and p a predicate on α. The map that sends each element of the subtype {x ∈ α | p(x)} to its underlying value x ∈ α is monotone; i.e., Subtype.val is an order-preserving map from {x ∈ α | p(x)} to α.
Русский
Пусть α упорядочено, p — предикат на α. Отображение, отправляющее каждый элемент подтипа {x ∈ α | p(x)} к соответствующему значению x ∈ α, монотонно: Subtype.val сохраняет порядок.
LaTeX
$$$\\forall a,b\\in\\{x:\\\\alpha \\mid p(x)\\},\\\\ a\\le b \\\\Rightarrow \\\\operatorname{val}(a)\\le \\operatorname{val}(b).$$$
Lean4
/-- `Subtype.val` as a bundled monotone function. -/
@[simps -fullyApplied]
def val (p : α → Prop) : Subtype p →o α :=
⟨_root_.Subtype.val, fun _ _ h => h⟩
