OAI/Analysis/CircleDomains/Reflection/ReflectionTileAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact action of a generating reflection on reduced words and their geometric tiles, including cancellation of the leading generator.

  1. def OAI.CircleDomainRigidity.reflectionReduceStep line 12
  2. lemma OAI.CircleDomainRigidity.reflectionReduceStep_isChain line 16
  3. lemma OAI.CircleDomainRigidity.reflectionReduceStep_involutive line 25
  4. lemma OAI.CircleDomainRigidity.reflectionWord_reduceStep line 39
  5. lemma OAI.CircleDomainRigidity.reflectionTile_reduceStep line 51
  6. lemma OAI.CircleDomainRigidity.reflection_tiles_union_invariant line 58