English
For a convex 𝕜-set s and a convex cone C, the hull of s is disjoint from C if and only if s is disjoint from the carrier of C.
Русский
Для выпуклого множества s и конуса C вершины оболочки hull 𝕜 s и C не пересекаются тогда и только тогда, когда множество s не пересекается с носителем конуса C.
LaTeX
$$$\\mathrm{Disjoint}(\\mathrm{hull}_{\\mathbb{K}}(s), C) \\iff \\mathrm{Disjoint}(s, |C|)$$$
Lean4
theorem disjoint_hull_left_of_convex (hs : Convex 𝕜 s) : Disjoint (hull 𝕜 s) C ↔ Disjoint s C
where
mp := by rw [← disjoint_coe]; exact .mono_left subset_hull
mpr := by
simp_rw [← disjoint_coe, disjoint_left, SetLike.mem_coe, mem_hull_of_convex hs]
rintro hsC _ ⟨r, hr, y, hy, rfl⟩
exact (C.smul_mem_iff hr).not.mpr (hsC hy)