OAI/Combinatorics/EditApproximation/Refinement/PhysicalFamilyTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal finite scalar family supplies the independent common source trace and its final draw, after removing unused extra copies.

  1. def OAI.EditApproximation.physicalFamilyToTrace line 23
  2. theorem OAI.EditApproximation.physicalFamilyToTrace_law line 33