sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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