OAI/Analysis/CircleDomains/Reflection/UpperSemidisk.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The fixed half disks used in the local boundary argument.

  1. def OAI.CircleDomainRigidity.upperSemidisk line 12
  2. lemma OAI.CircleDomainRigidity.upperSemidisk_open line 14
  3. lemma OAI.CircleDomainRigidity.upperSemidisk_convex line 17
  4. lemma OAI.CircleDomainRigidity.upperSemidisk_nonempty line 20
  5. lemma OAI.CircleDomainRigidity.upperSemidisk_closure_subset line 28
  6. lemma OAI.CircleDomainRigidity.upperSemidisk_compact_closure line 35
  7. lemma OAI.CircleDomainRigidity.upperSemidisk_frontier_nonempty line 39
  8. lemma OAI.CircleDomainRigidity.upperSemidisk_frontier_cases line 47