OAI/Analysis/CircleDomains/Topology/RelativePlateauNeighborhoods.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Plateau refinement for relatively closed sets in the physical domain, including terminal collars that reach deleted boundary components.

  1. def OAI.CircleDomainRigidity.relativePlateauNeighborhood line 12
  2. theorem OAI.CircleDomainRigidity.isOpen_relativePlateauNeighborhood line 17
  3. theorem OAI.CircleDomainRigidity.self_mem_relativePlateauNeighborhood line 24
  4. theorem OAI.CircleDomainRigidity.relativePlateauNeighborhood_subset_of_meets line 31
  5. theorem OAI.CircleDomainRigidity.partition_samples_within_relative_plateau line 41