OAI/Analysis/LipschitzHilbert/Phase/AngularExceptionCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The unshrunk path child costs at most one additional retained cell.

  1. theorem OAI.LipschitzHilbert.AngularGrid.independent_cells_card_le_one_exception line 13