OAI/Probability/CriticalPercolation/GraphTopology/LocalProjectiveTopology.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalPercolation.LocalProjective.NZ line 13
2. instance OAI.CriticalPercolation.LocalProjective.nzMulAction line 15
3. instance OAI.CriticalPercolation.LocalProjective.nzContinuousConstSMul line 20
4. abbrev OAI.CriticalPercolation.LocalProjective.Space line 23
5. def OAI.CriticalPercolation.LocalProjective.point line 24
6. lemma OAI.CriticalPercolation.LocalProjective.point_surjective line 26
7. lemma OAI.CriticalPercolation.LocalProjective.continuous_point line 27
8. lemma OAI.CriticalPercolation.LocalProjective.openQuotient_point line 28
9. lemma OAI.CriticalPercolation.LocalProjective.point_eq_iff line 32
10. lemma OAI.CriticalPercolation.LocalProjective.point_eq_iff_dependent line 43
11. instance OAI.CriticalPercolation.LocalProjective.spaceT2 line 54
12. instance OAI.CriticalPercolation.LocalProjective.spaceCompact line 65
13. instance OAI.CriticalPercolation.LocalProjective.spaceSecondCountable line 90
14. instance OAI.CriticalPercolation.LocalProjective.spaceMetrizable line 95