OAI/Analysis/OInfinity/ConnectedHalfFlipGenerators.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Connected conjugacy on a dense family of star-polynomial generators extends to finite subsets. The same witnessing unitary and path are retained.

  1. theorem OAI.WeakPureInfiniteness.connectedConjugacy_of_generators line 15
  2. theorem OAI.WeakPureInfiniteness.connectedHalfFlip_of_generators line 83
  3. theorem OAI.WeakPureInfiniteness.oInfinity_connectedHalfFlip_of_generators line 97