OAI/NumberTheory/Jacobsthal/Paths/ExpandedHardCapture.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.RegularStoppedMass.uncaptured_mass_le_exceptions line 21
2. theorem OAI.Erdos970.NumberTheoryLean.StoppedGeometryInvariance.traces_eq_of_geometry line 55
3. theorem OAI.Erdos970.NumberTheoryLean.StoppedGeometryInvariance.root_stopped_independent line 72
4. theorem OAI.Erdos970.NumberTheoryLean.StoppedGeometryInvariance.hasSourceStop_iff_original_root line 77
5. theorem OAI.Erdos970.NumberTheoryLean.ExpandedNoStop.expanded_no_lower_stop line 99
6. theorem OAI.Erdos970.NumberTheoryLean.ExpandedNoStop.expanded_no_stopped_prefix line 134
7. theorem OAI.Erdos970.NumberTheoryLean.ExpandedNoStop.expanded_no_source_stop line 140
8. theorem OAI.Erdos970.NumberTheoryLean.PaperRegularStopping.paper_regular_uncaptured_mass line 163
9. theorem OAI.Erdos970.NumberTheoryLean.ExpandedHardCapture.expanded_listed_subset_uncaptured line 225
10. theorem OAI.Erdos970.NumberTheoryLean.ExpandedHardCapture.expanded_listed_mass_le line 242