OAI/Probability/BenjaminiSchramm/FreshSlabCrossing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Percolation.BenjaminiSchramm.conn_internalEdges_end_mem line 13
2. def OAI.Percolation.BenjaminiSchramm.lowerCrossingBlock line 21
3. lemma OAI.Percolation.BenjaminiSchramm.lowerCrossingBlock_disjoint_upper line 24
4. lemma OAI.Percolation.BenjaminiSchramm.first_height_crossing_unexposed line 28
5. theorem OAI.Percolation.BenjaminiSchramm.conn_above_lower_first_crossing line 60