add_smul_mem — Mathlib

English

If hs is star-convex at 0 and x belongs to s, then for any t ≥ 1, x ∈ t·s.

Русский

Если s звёздочно выпукло относительно 0 и x ∈ s, то для любого t ≥ 1 верно x ∈ t·s.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(0,s) \\wedge x\\in s \\Rightarrow \\forall t\\ge 1:\\ x\\in t\\cdot s$$$

Lean4

theorem add_smul_mem (hs : StarConvex 𝕜 x s) (hy : x + y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : x + t • y ∈ s :=
  by
  have h : x + t • y = (1 - t) • x + t • (x + y) := by rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
  rw [h]
  exact hs hy (sub_nonneg_of_le ht₁) ht₀ (sub_add_cancel _ _)

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