OAI/Analysis/CircleDomains/Topology/QuotientInteriorBalls.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A physical ball compactly contained in the domain descends to an open quotient neighborhood with exactly that ball as its full inverse image.

  1. theorem OAI.CircleDomainRigidity.component_collapse_preimage_image_subset_domain line 18
  2. theorem OAI.CircleDomainRigidity.quotient_interior_ball line 33