OAI/Analysis/CircleDomains/Reflection/RoundExteriorChartSides.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The circular boundary chart has the exact two sides: its closed lower half maps into the closed disk, and its strict upper half maps outside it.

  1. lemma OAI.CircleDomainRigidity.unitExteriorBoundaryChart_norm_le_one line 12
  2. lemma OAI.CircleDomainRigidity.roundExteriorBoundaryChart_mem_closedBall line 26
  3. lemma OAI.CircleDomainRigidity.roundExteriorBoundaryChart_outside_iff line 33