strictMono — Mathlib

English

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

Русский

Если f строго монотонна на s, то f ∘ Subtype.val на s строго монотонна.

LaTeX

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

Lean4

protected theorem _root_.StrictMonoOn.strictMono (h : StrictMonoOn f s) : StrictMono (f ∘ Subtype.val : s → β) :=
  fun x y hlt => h x.coe_prop y.coe_prop hlt

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