sub — Mathlib

English

If hf: UniformConvexOn s φ f and hg: UniformConcaveOn s ψ g, then hf.sub hg yields UniformConvexOn s (φ+ψ) (f - g).

Русский

Если hf: UniformConvexOn s φ f и hg: UniformConcaveOn s ψ g, то hf.sub hg даёт UniformConvexOn s (φ+ψ) (f - g).

LaTeX

$$$$ \text{UniformConvexOn}(s,\phi,f) \land \text{UniformConcaveOn}(s,\psi,g) \Rightarrow \text{UniformConvexOn}(s,\phi+\psi,f-g). $$$$

Lean4

theorem sub (hf : UniformConvexOn s φ f) (hg : UniformConcaveOn s ψ g) : UniformConvexOn s (φ + ψ) (f - g) := by
  simpa using hf.add hg.neg

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