OAI/Analysis/CircleDomains/Topology/CompactScalarModel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar models with a globally deformed round complement. This is the smaller class needed for coefficient extremality: it contains the actual circle models and is closed under plane homeomorphisms. The deformation retains every complementary component, rather than just its boundary.

  1. structure OAI.CircleDomainRigidity.CompactScalarModel line 18
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.normalized line 44
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.image_open line 48
  4. theorem OAI.CircleDomainRigidity.CompactScalarModel.image_connected line 53
  5. theorem OAI.CircleDomainRigidity.CompactScalarModel.scalar_continuous line 58