OAI/Analysis/BiholderTransport/Regularity/LimitGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.continuous_graphProjection_family line 22
2. lemma OAI.WeakMTWTransport.graph_global_min_at_left_limit line 27
3. lemma OAI.WeakMTWTransport.WeakMTW.active_hull_nonconjugate_of_minimizing line 54
4. lemma OAI.WeakMTWTransport.active_hull_interior_below_minimizing line 75
5. lemma OAI.WeakMTWTransport.isPreconnected_fiber_of_mem_closure_bijective line 90
6. lemma OAI.WeakMTWTransport.fiber_subsingleton_of_preconnected_isolated line 144