mono — Mathlib

English

If m ≤ n and f is StrongConvexOn on s with parameter n, then f is StrongConvexOn on s with parameter m.

Русский

Если m ≤ n и функция строгоконвексна на s с параметром n, тогда она строгоконвексна на s с параметром m.

LaTeX

$$$$ (m \le n) \Rightarrow (\text{StrongConvexOn}(s,n,f) \Rightarrow \text{StrongConvexOn}(s,m,f)). $$$$

Lean4

nonrec theorem mono (hmn : m ≤ n) (hf : StrongConvexOn s n f) : StrongConvexOn s m f :=
  hf.mono fun r ↦ by gcongr

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