OAI/Analysis/WeakInfiniteness/IntertwiningConstruction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.FiniteIntertwining line 29
  2. structure OAI.WeakPureInfiniteness.IntertwiningState line 35
  3. def OAI.WeakPureInfiniteness.IntertwiningState.map line 40
  4. def OAI.WeakPureInfiniteness.IntertwiningStep line 43
  5. lemma OAI.WeakPureInfiniteness.exists_intertwiningStep line 49
  6. def OAI.WeakPureInfiniteness.intertwiningStages line 78
  7. lemma OAI.WeakPureInfiniteness.intertwiningStages_step line 83
  8. lemma OAI.WeakPureInfiniteness.intertwiningStages_tests_mono line 88
  9. lemma OAI.WeakPureInfiniteness.intertwiningStages_isometry line 94
  10. lemma OAI.WeakPureInfiniteness.intertwiningStages_cauchy_test line 100
  11. lemma OAI.WeakPureInfiniteness.intertwiningStages_cauchy line 114