OAI/Combinatorics/EditApproximation/Refinement/PhysicalFamilyMemo.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite family is consumed through actual source reads in the shared memo evaluator. Its final value and law agree with the proved local answer.

  1. theorem OAI.EditApproximation.physicalFamilyMemoResult_value line 36
  2. def OAI.EditApproximation.physicalFamilyMemoAnswer line 61
  3. theorem OAI.EditApproximation.physicalFamilyMemoAnswer_eq line 66
  4. theorem OAI.EditApproximation.physicalFamilyMemoAnswer_law line 75