OAI/Analysis/CircleDomains/Probability/ClosedFusionScheme.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Nested closed sets with uniformly shrinking children give a continuous branch-limit map on Baire space. This is the topological part of law fusion.

  1. structure OAI.CircleDomainRigidity.ClosedFusionScheme line 16
  2. theorem OAI.CircleDomainRigidity.ClosedFusionScheme.vanishingDiam line 28
  3. theorem OAI.CircleDomainRigidity.ClosedFusionScheme.total line 45
  4. def OAI.CircleDomainRigidity.ClosedFusionScheme.limit line 49
  5. theorem OAI.CircleDomainRigidity.ClosedFusionScheme.limit_mem line 52
  6. theorem OAI.CircleDomainRigidity.ClosedFusionScheme.continuous_limit line 55