OAI/Combinatorics/EditApproximation/Queries/QueryLocalBand.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mass and initial words are read into counted finite buffers before any random source range or local action is constructed.

  1. def OAI.EditApproximation.queryLocalBand line 26
  2. theorem OAI.EditApproximation.queryLocalBand_refines line 38