OAI/Analysis/CircleDomains/Topology/GatedQuotientMap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized map on the quotient domain. Its finite physical formula is required only over the bounded target gate, which misses infinity.

  1. def OAI.CircleDomainRigidity.quotientNormalizedMap line 15
  2. theorem OAI.CircleDomainRigidity.quotientNormalizedMap_continuous line 18
  3. theorem OAI.CircleDomainRigidity.quotientNormalizedMap_finite_gate line 24
  4. theorem OAI.CircleDomainRigidity.quotientNormalizedMap_physical line 40
  5. theorem OAI.CircleDomainRigidity.exists_uniform_infDist_gap line 49