OAI/Analysis/CircleDomains/Topology/PhysicalBoundaryGate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original gate on physical arc starts gives the required lower bound for the actual physical collar. The inverse quotient map is used only on its homeomorphic domain.

  1. theorem OAI.CircleDomainRigidity.physicalValue_quotient line 24
  2. theorem OAI.CircleDomainRigidity.compact_startingLaw_physical_gate line 32