English
Let s and t be disjoint convex sets with s compact and t closed in a locally convex space. Then there exist open convex neighborhoods U of s and V of t such that s ⊆ U, t ⊆ V, and U and V are disjoint.
Русский
Пусть s и t — непересекающиеся выпуклые множества в локально выпуклом пространстве; если s компактно, а t замкнуто, то существуют открытые выпуклые окрестности U и V с s ⊆ U, t ⊆ V и U ∩ V = ∅.
LaTeX
$$$\text{Disjoint}(s,t) \wedge \text{Convex}(s) \wedge \text{IsCompact}(s) \wedge \text{Convex}(t) \wedge \text{IsClosed}(t) \Rightarrow \exists U\exists V,\; \text{IsOpen}(U)\land \text{IsOpen}(V)\land \text{Convex}(U)\land \text{Convex}(V)\land s\subseteq U\land t\subseteq V\land \text{Disjoint}(U,V).$$$
Lean4
/-- In a locally convex space, every two disjoint convex sets such that one is compact and the other
is closed admit disjoint convex open neighborhoods. -/
theorem exists_open_convexes (disj : Disjoint s t) (hs₁ : Convex 𝕜 s) (hs₂ : IsCompact s) (ht₁ : Convex 𝕜 t)
(ht₂ : IsClosed t) : ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v :=
by
letI : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
rw [← uniformity_eq_comap_nhds_zero] at this
rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
refine
⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex, subset_add_left _ hV0,
subset_add_left _ hV0, ?_⟩
simp_rw [← iUnion_add_left_image, image_add_left]
simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
exact hV
