OAI/Geometry/Borsuk/Support/SupportIncidence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SupportFace line 13
2. lemma OAI.BorsukNine.SupportFace.mono line 16
3. lemma OAI.BorsukNine.exists_unit_orthogonal_dim line 21
4. lemma OAI.BorsukNine.Admissible.exists_label_absent_dim line 38
5. lemma OAI.BorsukNine.Admissible.support_card_three_le_of_card line 49
6. lemma OAI.BorsukNine.Admissible.support_extends_three_of_card line 66
7. lemma OAI.BorsukNine.Admissible.face_extends_three line 77
8. lemma OAI.BorsukNine.Admissible.triangle_no_free_edge line 84