OAI/Geometry/WeakMTW/Support/ActiveCollisionExclusion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakMTWGlobalSupport.WeakMTW.ActivePoint line 24
2. def OAI.WeakMTWGlobalSupport.WeakMTW.activeProjection line 26
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeProjection_continuous line 29
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.tendsto_ite_same line 33
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.active_collision_same_limit_false line 41
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.active_collision_exclusion line 84