English
If s is a convex subset of a vector space over 𝕜, then the cone hull hull 𝕜 s consists precisely of those vectors that lie on a positive scalar multiple of s; equivalently, x ∈ hull 𝕜 s iff there exists r > 0 with x ∈ r • s.
Русский
Если s — выпуклое множество в векторном пространстве над 𝕜, то конусная оболочка hull 𝕜 s состоит точно из тех векторов, которые лежат на положительном кратном множества s; эквивалентно, x ∈ hull 𝕜 s тогда и только тогда, когда существует r > 0, такое что x ∈ r • s.
LaTeX
$$$x \\in \\mathrm{hull}_{\\mathbb{K}}(s) \\iff \\exists r \\in \\mathbb{K},\\ 0 < r \\land x \\in r \\cdot s$$$
Lean4
/-- The cone hull of a convex set is simply the union of the open halflines through that set. -/
theorem mem_hull_of_convex (hs : Convex 𝕜 s) : x ∈ hull 𝕜 s ↔ ∃ r : 𝕜, 0 < r ∧ x ∈ r • s
where
mp
hx :=
hull_min (C :=
{ carrier := {y | ∃ r : 𝕜, 0 < r ∧ y ∈ r • s}
smul_mem' := by
intro r₁ hr₁ y ⟨r₂, hr₂, hy⟩
refine ⟨r₁ * r₂, mul_pos hr₁ hr₂, ?_⟩
rw [mul_smul]
exact smul_mem_smul_set hy
add_mem' := by
rintro y₁ ⟨r₁, hr₁, hy₁⟩ y₂ ⟨r₂, hr₂, hy₂⟩
refine ⟨r₁ + r₂, add_pos hr₁ hr₂, ?_⟩
rw [hs.add_smul hr₁.le hr₂.le]
exact add_mem_add hy₁ hy₂ })
(fun y hy ↦ ⟨1, by simpa⟩) hx
mpr := by rintro ⟨r, hr, y, hy, rfl⟩; exact (hull 𝕜 s).smul_mem hr <| subset_hull hy
