OAI/Probability/CriticalPercolation/Growth/CosetNormalClosure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.RelativeGrowth.boundedConjugates line 14
2. def OAI.CriticalPercolation.RelativeGrowth.conjugateStage line 17
3. lemma OAI.CriticalPercolation.RelativeGrowth.mem_boundedConjugates line 20
4. lemma OAI.CriticalPercolation.RelativeGrowth.boundedConjugates_mono line 24
5. lemma OAI.CriticalPercolation.RelativeGrowth.conjugateStage_mono line 31
6. lemma OAI.CriticalPercolation.RelativeGrowth.boundedConjugates_subset_pow line 36
7. lemma OAI.CriticalPercolation.RelativeGrowth.conjugateStage_le_normalClosure line 48
8. lemma OAI.CriticalPercolation.RelativeGrowth.conjugateStage_conj_generator line 55
9. lemma OAI.CriticalPercolation.RelativeGrowth.conjugateStage_normal_of_stationary line 72
10. lemma OAI.CriticalPercolation.RelativeGrowth.normalClosure_eq_conjugateStage_of_stationary line 93
11. theorem OAI.CriticalPercolation.RelativeGrowth.exists_conjugateStage_stationary line 106