OAI/Analysis/CircleDomains/Reflection/ReflectionTiles.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Disjoint reflected copies of the exterior of finitely many disjoint caps. Only the elementary side swapping and involution of each reflection are used.

  1. def OAI.CircleDomainRigidity.reflectionWord line 14
  2. def OAI.CircleDomainRigidity.reflectionTile line 18
  3. lemma OAI.CircleDomainRigidity.reflectionTile_nil line 21
  4. lemma OAI.CircleDomainRigidity.reflectionTile_cons line 25
  5. lemma OAI.CircleDomainRigidity.reflectionTile_cons_subset line 31
  6. lemma OAI.CircleDomainRigidity.reflectionTiles_pairwise_disjoint line 46