add — Mathlib

English

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

Русский

Если hf: UniformConcaveOn s φ f и hg: UniformConcaveOn s ψ g, то сложение даёт UniformConcaveOn s (φ+ψ) (f+g).

LaTeX

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

Lean4

theorem add (hf : UniformConcaveOn s φ f) (hg : UniformConcaveOn s ψ g) : UniformConcaveOn s (φ + ψ) (f + g) :=
  by
  refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
  simpa [mul_add, add_add_add_comm] using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)

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