OAI/Analysis/CircleDomains/Selection/SelectableRecursiveMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed recursive mean is compatible with the actual preceding selected presentations. Its physical coordinate and open exclusion are retained.

  1. theorem OAI.CircleDomainRigidity.RecursiveMeanOutput.selectable line 17