uniformConcaveOn_zero — Mathlib

English

Let s be a subset of a normed space E and f: E → ℝ. Then f is uniformly concave on s with modulus 0 if and only if f is concave on s.

Русский

Пусть s ⊆ E и f: E → ℝ. Тогда f является uniformly concave на s с модулем 0 тогда и только тогда, когда f выпукла/вогнута на s в обычном смысле (concaveOn).

LaTeX

$$$$ \mathrm{UniformConcaveOn}(s,0,f) \iff \mathrm{ConcaveOn}(\mathbb{R},s,f). $$$$

Lean4

@[simp]
theorem uniformConcaveOn_zero : UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f := by simp [UniformConcaveOn, ConcaveOn]

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