OAI/Analysis/CircleDomains/Selection/CountableMixedStages.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual mixed transfers of a countable ordered coordinate family. The finite lists inherit the original order, and every prescribed mark and every coordinate is eventually included.

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