OAI/Geometry/Borsuk/Projectors/Within.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.BorsukNine.withinLabelsline 12 - lemma
OAI.BorsukNine.mem_withinLabelsline 13 - lemma
OAI.BorsukNine.withinLabels_cardline 15 - lemma
OAI.BorsukNine.withinLabels_complline 18 - lemma
OAI.BorsukNine.withinLabels_insertline 22 - lemma
OAI.BorsukNine.Admissible.facet_complement_exclusionline 31 - lemma
OAI.BorsukNine.restricted_face_imageline 46 - lemma
OAI.BorsukNine.Admissible.facet_six_propertiesline 56