OAI/Probability/CriticalPercolation/Exploration/Users.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CriticalPercolation.OrderedQuery.(instance at line 25) line 25
2. def OAI.CriticalPercolation.OrderedQuery.users line 28
3. def OAI.CriticalPercolation.OrderedQuery.otherUsers line 31
4. lemma OAI.CriticalPercolation.OrderedQuery.mem_users line 34
5. lemma OAI.CriticalPercolation.OrderedQuery.mem_otherUsers line 37
6. lemma OAI.CriticalPercolation.OrderedQuery.otherUsers_card line 41
7. lemma OAI.CriticalPercolation.OrderedQuery.visits_bit_mem line 49
8. lemma OAI.CriticalPercolation.OrderedQuery.otherUsers_card_le_three line 54
9. lemma OAI.CriticalPercolation.OrderedQuery.first_iff_no_prior line 60
10. lemma OAI.CriticalPercolation.OrderedQuery.fresh_order_node line 72