OAI/Analysis/CircleDomains/Selection/SelectedMixedMeanExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The selected mixed model excludes each retained mean test on the same original open neighborhood, after passing to the common countable set of marks.

  1. theorem OAI.CircleDomainRigidity.SelectedMixedModels.excludes_retained_mean line 26