OAI/Analysis/CircleDomains/Rigidity/CountableMaskedStages.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual finite 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_masked_stages line 16