OAI/Combinatorics/EditApproximation/Geometry/LocalRefinementQuery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A local refinement query first reads its finite earlier-history cover, then the shared current samples, and finally the selected actions. The continuation is allowed to choose the last list from earlier answers.

  1. theorem OAI.EditApproximation.historyInputCode_injective line 19
  2. theorem OAI.EditApproximation.localRefinementStepQuery_value line 42