OAI/Analysis/LipschitzHilbert/Trees/SourceBlockException.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choose the actual continuing path child when it exists. In the terminal block any existing child may be used as the graph exception, since the path drop is one. A genuinely empty child family remains a separate case.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_exists_path_exception line 14