English
If hf: UniformConvexOn s φ f and hg: UniformConvexOn s ψ g, then hf.add hg yields UniformConvexOn s (φ+ψ) (f+g).
Русский
Если hf: UniformConvexOn s φ f и hg: UniformConvexOn s ψ g, то объединение с суммой модулей даёт UniformConvexOn s (φ+ψ) (f+g).
LaTeX
$$$$ \text{UniformConvexOn}(s,\phi,f) \land \text{UniformConvexOn}(s,\psi,g) \Rightarrow \text{UniformConvexOn}(s,\phi+\psi,f+g). $$$$
Lean4
theorem add (hf : UniformConvexOn s φ f) (hg : UniformConvexOn s ψ g) : UniformConvexOn s (φ + ψ) (f + g) :=
by
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
simpa [mul_add, add_add_add_comm, sub_add_sub_comm] using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
