monotone — Mathlib

English

If f is monotone on s, then the restricted function f ∘ Subtype.val on s is monotone.

Русский

Если f монотонна на s, то функция f ∘ Subtype.val на s монотонна.

LaTeX

$$$\operatorname{MonotoneOn}(f,s) \Rightarrow \operatorname{Monotone}(f \circ \operatorname{Subtype.val} : s \to \beta)$$$

Lean4

protected theorem _root_.MonotoneOn.monotone (h : MonotoneOn f s) : Monotone (f ∘ Subtype.val : s → β) := fun x y hle =>
  h x.coe_prop y.coe_prop hle

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