OAI/Combinatorics/EditApproximation/Queries/QueryInitialGather.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The first adaptive gather executes its binary support construction after reading the parent value, then requests those keys in their original order. Its continuation receives only the stored words actually read.

  1. theorem OAI.EditApproximation.queryInitialGather_refines line 16
  2. theorem OAI.EditApproximation.queryInitialGather_work line 41