OAI/Combinatorics/EditApproximation/Queries/QueryWarmupProgram.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A warmup step uses two adaptive gathers. The first determines its representatives; the second requests exactly their distinct child states.

  1. theorem OAI.EditApproximation.queryWarmupProgram_refines line 23