OAI/Geometry/Borsuk/Support/FacetTangent.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.BorsukNine.facetTangentline 11 - lemma
OAI.BorsukNine.facetTangent_applyline 33 - lemma
OAI.BorsukNine.facetTangent_zero_outsideline 37 - lemma
OAI.BorsukNine.facetTangent_sumline 40 - lemma
OAI.BorsukNine.facetTangent_injectiveline 46