neg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem neg (hf : UniformConvexOn s φ f) : UniformConcaveOn 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'] using hf.2 hx hy ha hb hab

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