OAI/Geometry/Borsuk/Support/LocalMix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.Admissible.sum_on_support line 19
2. lemma OAI.BorsukNine.Admissible.extension_on_positiveLine line 28
3. lemma OAI.BorsukNine.Admissible.localBlockModel_eq_of_positiveLine line 38
4. def OAI.BorsukNine.localBlockMix line 50
5. lemma OAI.BorsukNine.Admissible.localBlockMix_sum line 54
6. lemma OAI.BorsukNine.Admissible.localBlockMix_ne_zero line 68
7. def OAI.BorsukNine.facetTail line 85
8. lemma OAI.BorsukNine.Admissible.localBlockMix_tangent_zero line 90
9. lemma OAI.BorsukNine.Admissible.localBlockMix_hit line 119