openSegment_subset_strict_hypograph

English

Dual statement for concave functions gives the open segment subset of the hypograph.

Русский

Дуальное утверждение для вогнутых функций: открытый сегмент принадлежит гипографу.

LaTeX

$$$\text{If } f \text{ is concave, then openSegment\,(p,q) } \subseteq \{(x,t): x\in s, t < f(x)\}$$$

Lean4

theorem openSegment_subset_strict_hypograph (hf : ConcaveOn 𝕜 s f) (p q : E × β) (hp : p.1 ∈ s ∧ p.2 < f p.1)
    (hq : q.1 ∈ s ∧ q.2 ≤ f q.1) : openSegment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ p.2 < f p.1} :=
  hf.dual.openSegment_subset_strict_epigraph p q hp hq

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