Connected components in compact spaces

A connected component in a compact Hausdorff space has arbitrarily small clopen neighborhoods. This is the compact-space separation fact used in the BPC argument.

theorem LeanPool.Besicovitch.IsPreconnected.preimage_subtype_of_subset {X : Type u_1} [TopologicalSpace X] {A Q : Set X} (hA : IsPreconnected A) (hAQ : A ⊆ Q) : IsPreconnected (Subtype.val ⁻¹' A)

A preconnected subset remains preconnected when viewed inside a larger subtype.

theorem LeanPool.Besicovitch.isCompact_connectedComponentIn {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (x : X) : IsCompact (connectedComponentIn K x)

A connected component cut out inside a compact set is compact.

theorem LeanPool.Besicovitch.exists_isClopen_between_connectedComponent {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hcomponent : connectedComponent x ⊆ U) : ∃ (H : Set X), IsClopen H ∧ connectedComponent x ⊆ H ∧ H ⊆ U

In a compact Hausdorff space, a connected component contained in an open set has a clopen neighborhood contained in that open set.

theorem LeanPool.Besicovitch.exists_isClopenWithin_between_connectedComponentIn_closedBall {X : Type u_1} [PseudoMetricSpace X] [T2Space X] {Q : Set X} (hQ : IsCompact Q) {z : X} (hzQ : z ∈ Q) {R rho : ℝ} (hR : 0 ≤ R) (hRrho : R < rho) (hcomponent : connectedComponentIn (Q ∩ Metric.closedBall z rho) z ⊆ Metric.ball z R) : ∃ (H : Set X), connectedComponentIn (Q ∩ Metric.closedBall z rho) z ⊆ H ∧ H ⊆ Q ∩ Metric.ball z R ∧ IsClopen (Subtype.val ⁻¹' H) ∧ IsCompact H

A clopen neighborhood of a component in a closed ball remains clopen in the ambient compact set when it lies in a strictly smaller ball.