add_smul_sub_mem — Mathlib

English

If s is star-convex at x and y ∈ s, with t in [0,1], then x + t·y ∈ s.

Русский

Если s звёздочно выпукло относительно x, и y ∈ s, и t ∈ [0,1], то x + t·y ∈ s.

LaTeX

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

Lean4

theorem add_smul_sub_mem (hs : StarConvex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) :
    x + t • (y - x) ∈ s := by
  apply hs.segment_subset hy
  rw [segment_eq_image']
  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

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