OAI/Analysis/CircleDomains/Uniformization/MixedLimitRealProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A mixed limit retains the exact real subfamily limit. Reindexing the finite terminal assignment preserves its point labels, so all previously proved real-barrier conclusions apply to this same limit map.

  1. theorem OAI.CircleDomainRigidity.PhysicalTerminalDisks.exists_reindexed_assignment line 15
  2. def OAI.CircleDomainRigidity.TerminalComponentAssignment.changeMap line 30
  3. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.changeMap_point line 38
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedMixedModelLimit.exists_real_assignment line 55
  5. def OAI.CircleDomainRigidity.FiniteTransfer.AssignedMixedModelLimit.toReal line 68