OAI/Analysis/CircleDomains/Uniformization/FiniteModelEnds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Terminal components of an actual finite circle model

Every physical terminal disk determines a target complementary component. The assignment exhausts all target components and respects every retained Jordan contour. Only the existing topological inputs are used.

  1. theorem OAI.CircleDomainRigidity.SmoothJordanCore.boundary_subset_domain line 24
  2. theorem OAI.CircleDomainRigidity.jordan_address_eq_of_common_point line 34
  3. theorem OAI.CircleDomainRigidity.exists_finite_model_terminal_assignment line 45