convex_segment — Mathlib

English

The segment [x,y] is convex in E when 𝕜 is an ordered ring.

Русский

Отрезок [x,y] выпукл в пространстве E при упорядоченной кольцевой структуре 𝕜.

LaTeX

$$$\Convex 𝕜 [\,x- [𝕜] y\]$$$

Lean4

theorem convex_segment [IsOrderedRing 𝕜] (x y : E) : Convex 𝕜 [x -[𝕜] y] :=
  by
  rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab
  refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩
  · rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
  · match_scalars <;> noncomm_ring

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