CollapseRelation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Closedness of the component-collapse relation

The connected-component space of a closed set in a compact Hausdorff space is compact Hausdorff. Collapsing its components gives a closed relation, as required by Moore's sphere decomposition theorem.

theorem OAI.CircleDomainRigidity.isClosed_componentCollapseRelation line 20

Source documentation

Collapsing the connected components of a closed set in a compact Hausdorff space, and leaving the remaining points fixed, gives a closed relation.

theorem isClosed_componentCollapseRelation
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    {F : Set X} (hF : IsClosed F) :
    IsClosed {p : X × X | p.1 = p.2 ∨
      (p.1 ∈ F ∧ p.2 ∈ connectedComponentIn F p.1)} := by
…