mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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