openSegment_subset_strict_epigraph

English

Open segments lie inside the epigraph region for convexity considerations.

Русский

Открытые отрезки содержатся в эпиграфе для выпуклости.

LaTeX

$$$\text{Given convex } s,\; p,q,\; \text{openSegment}(p,q) \subseteq \{(x,t): x\in s, t \ge f(x)\}$$$

Lean4

theorem openSegment_subset_strict_epigraph (hf : ConvexOn 𝕜 s f) (p q : E × β) (hp : p.1 ∈ s ∧ f p.1 < p.2)
    (hq : q.1 ∈ s ∧ f q.1 ≤ q.2) : openSegment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} :=
  by
  rintro _ ⟨a, b, ha, hb, hab, rfl⟩
  refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩
  calc
    f (a • p.1 + b • q.1) ≤ a • f p.1 + b • f q.1 := hf.2 hp.1 hq.1 ha.le hb.le hab
    _ < a • p.2 + b • q.2 :=
      add_lt_add_of_lt_of_le (smul_lt_smul_of_pos_left hp.2 ha) (smul_le_smul_of_nonneg_left hq.2 hb.le)

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