OAI/Analysis/CircleDomains/Modulus/WeightedCollarNeighborhoods.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Weighted collars in the physical plane and their actual open quotient neighborhoods. Compact containment survives projection.

  1. structure OAI.CircleDomainRigidity.WeightedCollar line 17
  2. def OAI.CircleDomainRigidity.WeightedCollar.region line 38
  3. theorem OAI.CircleDomainRigidity.WeightedCollar.isOpen_region line 40
  4. theorem OAI.CircleDomainRigidity.WeightedCollar.point_mem_region line 46
  5. theorem OAI.CircleDomainRigidity.WeightedCollar.closure_region_subset_image line 53
  6. theorem OAI.CircleDomainRigidity.WeightedCollar.closure_region_subset line 58
  7. theorem OAI.CircleDomainRigidity.WeightedCollar.frontier_region_subset line 65
  8. theorem OAI.CircleDomainRigidity.exists_weighted_collar_in_neighborhood line 80