OAI/Probability/CriticalPercolation/Growth/CosetTransfer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.RelativeGrowth.subgroupCosetEmbedding line 14
2. lemma OAI.CriticalPercolation.RelativeGrowth.subgroupCosetEmbedding_mk line 24
3. lemma OAI.CriticalPercolation.RelativeGrowth.subgroupCosetEmbedding_range line 26
4. lemma OAI.CriticalPercolation.RelativeGrowth.finite_coset_image_subgroup_iff line 35
5. lemma OAI.CriticalPercolation.RelativeGrowth.bounded_subgroup_iff line 43
6. lemma OAI.CriticalPercolation.RelativeGrowth.subgroup_ball_image line 51
7. lemma OAI.CriticalPercolation.RelativeGrowth.HasDegree.subgroup_bounded line 57
8. lemma OAI.CriticalPercolation.RelativeGrowth.finite_image_of_finite_coset_image line 75
9. lemma OAI.CriticalPercolation.RelativeGrowth.finiteIndex_bounded_generators line 86