OAI/Analysis/HardSphere/Geometry/AvoidanceReflectionNorm.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HardSphere.avoidance_reflection_normline 18 - lemma
OAI.HardSphere.free_deficit_le_twice_killedline 32