OAI/Analysis/CircleDomains/Transfer/SelectedMixedModels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The countable selected family produces actual mixed finite models. Every chosen real presentation, including a real barrier selected after the seed, is retained with its exact physical and quotient functions. The finite coordinates keep the selected family's order.

  1. structure OAI.CircleDomainRigidity.SelectedMixedModels line 22
  2. theorem OAI.CircleDomainRigidity.exists_selected_mixed_models line 52