OAI/Analysis/HardSphere/Geometry/ParentStep.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.BathSlice.parent_step line 20
2. lemma OAI.HardSphere.BathSlice.parent_fiber_finite line 36
3. lemma OAI.HardSphere.BathSlice.parent_preimage_finite line 55
4. lemma OAI.HardSphere.BathSlice.parent_reach line 63
5. lemma OAI.HardSphere.BathSlice.parent_projection_reachable line 74
6. lemma OAI.HardSphere.Lattice.badGraph_reachable_induce line 95
7. lemma OAI.HardSphere.Lattice.badComponent_preconnected line 103
8. theorem OAI.HardSphere.BathSlice.parent_component_lift line 116
9. theorem OAI.HardSphere.BathSlice.finite_of_parent_component_small line 142
10. lemma OAI.HardSphere.Lattice.liftedBadComponent_eq_of_mem line 153
11. lemma OAI.HardSphere.Lattice.own_badComponent_card_lt line 162