OAI/Analysis/RieszRectifiability/Restart/SelectedRestartTree.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.RieszRectifiability.relativeRestartGoodline 17 - def
OAI.RieszRectifiability.relativeSelectedRestartStopsline 22 - def
OAI.RieszRectifiability.selectedRestartParentline 29 - def
OAI.RieszRectifiability.selectedRestartRemainderline 33 - def
OAI.RieszRectifiability.selectedRestartNextline 38 - theorem
OAI.RieszRectifiability.selected_restart_child_is_restartline 45 - theorem
OAI.RieszRectifiability.selected_restart_next_consumes_bad_cellline 59 - theorem
OAI.RieszRectifiability.selected_restart_partitionline 82