OAI/Geometry/Borsuk/LocalParity/LocalModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.Admissible.signedExtension_kernel_coordinate line 18
2. def OAI.BorsukNine.localBlockModel line 26
3. lemma OAI.BorsukNine.localBlockModel_odd line 31
4. lemma OAI.BorsukNine.Admissible.localBlockModel_continuousOn line 38
5. lemma OAI.BorsukNine.Admissible.localBlockModel_on_facet line 48
6. lemma OAI.BorsukNine.Admissible.localBlockModel_sum_facet line 57
7. lemma OAI.BorsukNine.Admissible.localBlockModel_ne_zero line 74