OAI/Analysis/CircleDomains/Uniformization/AssignedParameterLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalized finite models retaining marked disk parameters

This assembles the published normal-family inputs, the constructed finite terminal assignment, the actual smooth Jordan exhaustion, and marked-disk trapping. Every marked limit is attached to its source component.

  1. theorem OAI.CircleDomainRigidity.exists_normalized_limit_with_assigned_parameters line 23