OAI/Analysis/CircleDomains/Uniformization/RecursiveLimitIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized recursive limit is the identity when the source complement is removable. Its sphere extension and orientation are proved from matched ends; neither is a separate assumption.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.recursive_limit_eq_id line 24