mono — Mathlib

English

If ψ ≤ φ and f is uniformly concave on s with modulus φ, then f is uniformly concave on s with modulus ψ.

Русский

Пусть ψ ≤ φ и f выпукла(uniform concave) на s с модулем φ; тогда f выпукла на s с модулем ψ.

LaTeX

$$$$ (\psi \le \phi) \Rightarrow (\text{UniformConcaveOn}(s,\phi,f) \Rightarrow \text{UniformConcaveOn}(s,\psi,f)). $$$$

Lean4

theorem mono (hψφ : ψ ≤ φ) (hf : UniformConcaveOn s φ f) : UniformConcaveOn s ψ f :=
  ⟨hf.1, fun x hx y hy a b ha hb hab ↦ (hf.2 hx hy ha hb hab).trans' <| by gcongr; apply hψφ⟩

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