OAI/Geometry/Cannon/ScalarLimits/ConnectedLimit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonContinuumLimit.connected_limit line 31
2. lemma OAI.CannonContinuumLimit.diam_le_add_dist line 70
3. lemma OAI.CannonContinuumLimit.diameter_limit line 88
4. lemma OAI.CannonContinuumLimit.approximating_points line 101
5. lemma OAI.CannonContinuumLimit.level_limit line 112
6. lemma OAI.CannonContinuumLimit.closed_meeting_limit line 127
7. theorem OAI.CannonContinuumLimit.continuum_subsequence line 134
8. theorem OAI.CannonContinuumLimit.domain_level_limit line 149
9. theorem OAI.CannonContinuumLimit.straddling_continua_limit line 174
10. theorem OAI.CannonApprox.constructed_scalar_continua line 215
11. lemma OAI.CannonMeasureOscillation.inverse_geometric_near line 266
12. lemma OAI.CannonMeasureOscillation.osc_sq_le_of_pairwise line 286
13. lemma OAI.CannonMeasureOscillation.compact_subtype_closedBall line 296
14. theorem OAI.CannonMeasureOscillation.annular_to_measure line 310