OAI/Analysis/CircleDomains/Modulus/NormalizedAssignedEnds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalized finite models with prescribed marked ends

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_ends line 23