OAI/Combinatorics/EditApproximation/Geometry/LocalWideStep.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One concrete refinement entry, using direct local representative and cell loops. Band data and previously gathered child tables are arguments; no complete current-index child table is enumerated.

  1. def OAI.EditApproximation.rationalLocalWideStep line 11
  2. theorem OAI.EditApproximation.rationalLocalWideStep_eq line 30
  3. theorem OAI.EditApproximation.rationalLocalWideStep_bounds line 55