English
In a compact T2 space, the connected component of a point equals the intersection of all clopen neighborhoods containing that point.
Русский
В компактном пространстве T2 компонент связи точки равен пересечению всех клипных окрестностей, содержащих эту точку.
LaTeX
$$$ \\text{connectedComponent}(x) = \\bigcap_{s : { s : Set X // IsClopen s \\land x \\in s },\\, s} s $ in a compact T2 space$$
Lean4
/-- In a compact T₂ space, the connected component of a point equals the intersection of all
its clopen neighbourhoods. -/
theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : X) :
connectedComponent x = ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s :=
by
apply Subset.antisymm connectedComponent_subset_iInter_isClopen
refine
IsPreconnected.subset_connectedComponent ?_
(mem_iInter.2 fun s => s.2.2)
-- We do this by showing that any disjoint cover by two closed sets implies
-- that one of these closed sets must contain our whole thing.
-- To reduce to the case where the cover is disjoint on all of `X` we need that `s` is closed
have hs : @IsClosed X _ (⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s) := isClosed_iInter fun s => s.2.1.1
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]
intro a b ha hb hab ab_disj
rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩
obtain ⟨s, H⟩ : ∃ s : Set X, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v := by
/- Now we find a clopen set `s` around `x`, contained in `u ∪ v`. We utilize the fact that
`X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods
of `X` disjoint to it, but a finite intersection of clopen sets is clopen,
so we let this be our `s`. -/
have H1 :=
(hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s)
fun s => s.2.1.1
rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1
obtain ⟨si, H2⟩ := H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)
refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩
· exact isClopen_biInter_finset fun s _ => s.2.1
· exact mem_iInter₂.2 fun s _ => s.2.2
·
rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty]
-- So, we get a disjoint decomposition `s = s ∩ u ∪ s ∩ v` of clopen sets. The intersection of all
-- clopen neighbourhoods will then lie in whichever of u or v x lies in and hence will be a subset
-- of either a or b.
· have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
rw [union_comm] at H
have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
by_cases hxu : x ∈ u <;> [left; right]
-- The x ∈ u case.
· suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u from
Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
· apply Subset.trans _ s.inter_subset_right
exact
iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩
-- If x ∉ u, we get x ∈ v since x ∈ u ∪ v. The rest is then like the x ∈ u case.
· have h1 : x ∈ v := (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v from
(huv.symm.mono this hau).left_le_of_le_sup_left hab
· refine Subset.trans ?_ s.inter_subset_right
exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1) ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩
