OAI/Combinatorics/EditApproximation/Queries/QueryRefinementGather.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The last three adaptive gathers of a refinement request. Each request list is constructed after the answers on which it depends. The selected actions, list construction, sorting and buffer cells all carry work.

  1. theorem OAI.EditApproximation.queryRefinementGather_work line 39
  2. theorem OAI.EditApproximation.queryRefinementGather_refines line 96