OAI/Analysis/CircleDomains/Rigidity/FiniteMatchedField.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual selected matched field is finite, measurable, and bounded on every compact part of the source plane.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.planeRelation_ne_infty line 20
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedTarget_finite line 33
  3. def OAI.CircleDomainRigidity.MatchedConformalEnds.selectedPlane line 38
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedPlane_measurable line 41
  5. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.compact_relation_finite_image line 79
  6. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedPlane_bounded_on_compact line 99