OAI/Geometry/PinnedDistances/FiniteObstruction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Bounded.no_finite_expanded line 11
2. lemma OAI.WeakPinned.Bounded.no_sphere_expanded line 48
3. def OAI.WeakPinned.Bounded.zEquation line 148
4. def OAI.WeakPinned.Bounded.wEquation line 150
5. lemma OAI.WeakPinned.Bounded.zEquation_closed line 153
6. lemma OAI.WeakPinned.Bounded.wEquation_closed line 154
7. lemma OAI.WeakPinned.Bounded.tripleWeight_mem line 157
8. lemma OAI.WeakPinned.Bounded.expanded_chart_zero line 165