OAI/Probability/SwitchChain/HavelInduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.HavelCanonical.exists_top_subset line 10
2. def OAI.Problem315.HavelCanonical.AgreeOutside line 40
3. theorem OAI.Problem315.HavelCanonical.residual_degree_eq line 43
4. theorem OAI.Problem315.HavelCanonical.agreeOutside_erase line 69
5. theorem OAI.Problem315.HavelCanonical.connected_of_row_alignment line 78
6. theorem OAI.Problem315.HavelCanonical.connected_of_neighborhood_repair line 117