OAI/NumberTheory/DukePrimeDegree/Dynamics/LeafReturnCovariance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Annular compact returns avoiding leafwise null exceptions

The simultaneous-return argument can also enforce any property holding almost everywhere on the common leaf. In particular both rebasing laws can be enforced, so equal initial leaves give equal terminal leaves at the chosen compact return.

  1. theorem OAI.DukePrimeDegree.exists_annular_simultaneous_root_return_ae line 21
  2. theorem OAI.DukePrimeDegree.exists_annular_return_with_equal_leaves line 64