mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mono (hψφ : ψ ≤ φ) (hf : UniformConvexOn s φ f) : UniformConvexOn 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ψφ⟩

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