OAI/Analysis/CircleDomains/Topology/BoundedAnalyticCollar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source collar is chosen with compact closure inside the analytic chart. Its physical image has one finite bound for every later model.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_bounded_analytic_boundary_collar line 15