ClopenNeighborhood.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Isolating a component by a clopen neighborhood

This is the compact-space step before the smooth contour construction: a neighborhood containing a whole component contains a clopen neighborhood of that component's base point. Applied in a closed obstacle set, it isolates a singleton dust component.

theorem OAI.CircleDomainRigidity.exists_clopen_between_component_and_open line 18

theorem OAI.CircleDomainRigidity.exists_clopen_neighborhood_of_singleton_component line 37

Source documentation

In particular, singleton components in a compact closed obstacle have arbitrarily small relatively clopen neighborhoods.

theorem exists_clopen_neighborhood_of_singleton_component
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    (x : X) (hC : connectedComponent x = {x}) {O : Set X}
    (hO : IsOpen O) (hx : x ∈ O) :
    ∃ V : Set X, IsClopen V ∧ x ∈ V ∧ V ⊆ O :=
…