neg — Mathlib

English

If hf: UniformConcaveOn s φ f, then UniformConvexOn s φ (-f).

Русский

Если hf: UniformConcaveOn s φ f, то UniformConvexOn s φ (-f).

LaTeX

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

Lean4

theorem neg (hf : UniformConcaveOn s φ f) : UniformConvexOn s φ (-f) :=
  by
  refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
  simpa [add_comm, -neg_le_neg_iff, ← le_sub_iff_add_le', sub_eq_add_neg, neg_add] using hf.2 hx hy ha hb hab

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