OAI/Analysis/CircleDomains/Transfer/GraphGeometricCompletion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cover the remaining quotient dust using the actual closed level sets of mixed real and period tests, after the physical collision terminals have been selected.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_geometric_completion_for_graphs line 16