OAI/Combinatorics/IndependentSets/Geometry/GeometryAntipodes.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.LargeIndependentSets.GeometryNames.antiPointline 14 - def
OAI.LargeIndependentSets.GeometryNames.antiNameline 17 - lemma
OAI.LargeIndependentSets.GeometryNames.antiName_exactline 21 - def
OAI.LargeIndependentSets.GeometryNames.antiExprline 26 - lemma
OAI.LargeIndependentSets.GeometryNames.antiExpr_evalline 31 - def
OAI.LargeIndependentSets.GeometryNames.payloadApplyline 53 - lemma
OAI.LargeIndependentSets.GeometryNames.payloadApply_evalline 55 - def
OAI.LargeIndependentSets.GeometryNames.antiDistanceExprline 60 - lemma
OAI.LargeIndependentSets.GeometryNames.antiDistanceExpr_evalline 62 - def
OAI.LargeIndependentSets.GeometryNames.cliqueExprline 69 - lemma
OAI.LargeIndependentSets.GeometryNames.cliqueExpr_nonzeroline 72