= Šura-Bura lemma
{c}
{title2=$C(x)=Q(x)$}
In a <compact Hausdorff space>, each <connected component> is its <quasi-component> and has a neighborhood basis of <clopen> sets. Let $Q$ be the <intersection> of <clopen> neighborhoods of $x$. It is <compact>. If it splits into two nonempty <compact> sets, normality separates them by disjoint <open neighborhoods>. The <finite intersection characterization of compactness> gives a finite <intersection> of <clopen> neighborhoods lying in their <union>. Its <intersection> with the neighborhood containing $x$ is then <clopen> and excludes part of $Q$, a contradiction. Thus $Q$ is <connected> and equals the component. Applying the same finite-intersection argument to any neighborhood of $Q$ proves the neighborhood-basis assertion. https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/browser_info/HOL/HOL-Analysis/Homotopy.html[Formalized Šura-Bura results, including the compact Euclidean case]{ref}.
Back to article page
