OAI/Probability/CriticalPercolation/Gluing/CorridorSeparation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CriticalPercolation.Corridor.Site line 13
  2. abbrev OAI.CriticalPercolation.Corridor.Point line 14
  3. abbrev OAI.CriticalPercolation.Corridor.Edge line 15
  4. def OAI.CriticalPercolation.Corridor.source line 17
  5. def OAI.CriticalPercolation.Corridor.target line 18
  6. def OAI.CriticalPercolation.Corridor.endpoints line 19
  7. def OAI.CriticalPercolation.Corridor.box line 21
  8. def OAI.CriticalPercolation.Corridor.tube line 24
  9. def OAI.CriticalPercolation.Corridor.domain line 29
  10. lemma OAI.CriticalPercolation.Corridor.int_eq_of_close line 32
  11. lemma OAI.CriticalPercolation.Corridor.int_endpoint_interval line 37
  12. lemma OAI.CriticalPercolation.Corridor.box_disjoint line 43
  13. lemma OAI.CriticalPercolation.Corridor.box_tube_endpoint line 55
  14. lemma OAI.CriticalPercolation.Corridor.tubes_opposite line 78
  15. lemma OAI.CriticalPercolation.Corridor.tubes_parallel_true line 92
  16. lemma OAI.CriticalPercolation.Corridor.tubes_parallel_false line 114
  17. lemma OAI.CriticalPercolation.Corridor.distinct_tubes_intersection line 136
  18. lemma OAI.CriticalPercolation.Corridor.box_domain_endpoint line 148
  19. theorem OAI.CriticalPercolation.Corridor.distinct_domains_intersection line 162
  20. lemma OAI.CriticalPercolation.Corridor.common_endpoint_unique line 173
  21. lemma OAI.CriticalPercolation.Corridor.incident_domains_intersection line 183
  22. lemma OAI.CriticalPercolation.Corridor.nonincident_domains_disjoint line 191
  23. lemma OAI.CriticalPercolation.Corridor.nonendpoint_domain_box_disjoint line 204
  24. lemma OAI.CriticalPercolation.Corridor.source_scales line 208