English
A separation principle ensures that the segment between certain points intersects a convex hull of a triangle formed by three points.
Русский
Принцип разделения обеспечивает пересечение отрезка между точками с выпуклым шаром треугольника из трёх точек.
LaTeX
$$Not disjoint: the segment between certain points intersects convexHull {p,q,z}.$$
Lean4
/-- **Stone's Separation Theorem** -/
theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hst : Disjoint s t) :
∃ C : Set E, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ :=
by
let S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
obtain ⟨C, hsC, hmax⟩ :=
zorn_subset_nonempty S
(fun c hcS hc ⟨_, _⟩ =>
⟨⋃₀ c, ⟨hc.directedOn.convex_sUnion fun s hs => (hcS hs).1, disjoint_sUnion_left.2 fun c hc => (hcS hc).2⟩,
fun s => subset_sUnion_of_mem⟩)
s ⟨hs, hst⟩
obtain hC : _ ∧ _ := hmax.prop
refine ⟨C, hC.1, convex_iff_segment_subset.2 fun x hx y hy z hz hzC => ?_, hsC, hC.2.subset_compl_left⟩
suffices h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
by
obtain ⟨p, hp, u, hu, hut⟩ := h x hx
obtain ⟨q, hq, v, hv, hvt⟩ := h y hy
refine
not_disjoint_segment_convexHull_triple hz hu hv
(hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min ?_ hC.1)
simp [insert_subset_iff, hp, hq, singleton_subset_iff.2 hzC]
rintro c hc
by_contra! h
suffices h : Disjoint (convexHull 𝕜 (insert c C)) t
by
rw [hmax.eq_of_subset ⟨convex_convexHull _ _, h⟩ <| (subset_insert ..).trans <| subset_convexHull ..] at hc
exact hc (subset_convexHull _ _ <| mem_insert _ _)
rw [convexHull_insert ⟨z, hzC⟩, convexJoin_singleton_left]
refine disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inter_eq_empty.2 (h a ?_)
rwa [← hC.1.convexHull_eq]
