convex_openSegment — Mathlib

English

The open segment between any two points in a convex set is itself convex.

Русский

Открытый отрезок между двумя точками внутри выпуклого множества снова выпуклый.

LaTeX

$$$$ \\text{Convex}_{\\mathbb{K}}(\\text{openSegment}_{\\mathbb{K}}(a,b)) $$$$

Lean4

theorem convex_openSegment (a b : E) : Convex 𝕜 (openSegment 𝕜 a b) :=
  by
  rw [convex_iff_openSegment_subset]
  rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ z ⟨a, b, ha, hb, hab, rfl⟩
  refine ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, ?_, ?_⟩
  · linear_combination (norm := noncomm_ring) a * habp + b * habq + hab
  · module

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