OAI/Analysis/CircleDomains/Topology/RecursiveCircleModels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Select actual circle models for the recursively constructed finite families, then extract their normalized conformal limit. The model supply in the intermediate construction is discharged by the published-input finite-list theorem below.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.exists_models_and_limit line 25
  2. theorem OAI.CircleDomainRigidity.exists_recursive_models_of_published_inputs line 48