OAI/Combinatorics/EditApproximation/Geometry/LocalGroupSourceQuery.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Whole-cell group samples are exposed through scalar source reads. Every needed scale/sample coordinate is enumerated once per group; unused groups are absent from this query.

  1. theorem OAI.EditApproximation.groupScalarKeys_mem line 17
  2. theorem OAI.EditApproximation.groupScalarKeys_length_le line 26
  3. def OAI.EditApproximation.groupScalarValue line 42
  4. theorem OAI.EditApproximation.groupDrawFromValues_eq line 47
  5. theorem OAI.EditApproximation.localCellGroupActions_congr_draw line 60
  6. def OAI.EditApproximation.localGroupSourceStepQuery line 87
  7. theorem OAI.EditApproximation.localGroupSourceStepQuery_value line 93