OAI/Analysis/CircleDomains/Uniformization/RealFiniteModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Principally normalized finite models with real coordinates

The actual real fillings remain real functions after composition with the smooth inverse of the normalized model. This specialization is used for the barrier coordinates, whose values zero and one must be retained.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_metric_model_with_real_fillings line 22