OAI/Analysis/HardSphere/Orbitals/CellPartition.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HardSphere.CellOrbital.gridHomeline 15 - lemma
OAI.HardSphere.CellOrbital.gridHome_measurableline 18 - lemma
OAI.HardSphere.CellOrbital.gridHome_memline 21 - lemma
OAI.HardSphere.CellOrbital.centeredCell_disjointline 39 - lemma
OAI.HardSphere.CellOrbital.gridHome_eq_iffline 59