OAI/Combinatorics/EditApproximation/Refinement/PhysicalComparisonBand.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Non-bad, low-velocity comparison children belong to an actual unskipped cell band.

  1. theorem OAI.EditApproximation.physicalComparison_unskipped line 40