OAI/Analysis/CircleDomains/Topology/CompactComponentPiece.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A whole component of a compact obstacle can be isolated inside any prescribed open neighborhood by a compact relatively clopen piece.

  1. lemma OAI.CircleDomainRigidity.exists_compact_piece_of_component line 11