add_smul_mem — Mathlib

English

If s is convex, then adding a point and a scaled version preserves membership under convex combinations.

Русский

Если s выпукло, то сумма точки и масштабированного элемента сохраняет выпуклость.

LaTeX

$$$$ \\text{Convex}_{\\mathbb{K}}(s) \\rightarrow \\text{add-smul} $$$$

Lean4

theorem add_smul_mem (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) :
    x + t • y ∈ s :=
  by
  have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring
  rw [h]
  exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)

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