OAI/Analysis/CircleDomains/Uniformization/ScalarPointwiseLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded scalar fillings converge at every point of the limiting image to the retained source scalar.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.filled_tendsto_on_image line 20
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.pointwise_on_image line 81