OAI/Combinatorics/EditApproximation/Queries/QueryFamilyActive.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Positive internal refinement steps expose exactly the independent scalar family and smaller physical table requests of the reference body.

  1. theorem OAI.EditApproximation.active_request_eq line 22
  2. def OAI.EditApproximation.queryFamilyActive line 29
  3. theorem OAI.EditApproximation.queryFamilyActive_refines line 41
  4. def OAI.EditApproximation.queryFamilyBoundedActive line 71
  5. theorem OAI.EditApproximation.queryFamilyBoundedActive_refines line 80