OAI/Analysis/CircleDomains/Reflection/MovingCircleReflectionLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the explicit reflected maps on a fixed two-sided collar. The bound is independent of the reciprocals of the target radii.

  1. lemma OAI.CircleDomainRigidity.exists_moving_circle_reflection_limit line 13
  2. lemma OAI.CircleDomainRigidity.moving_circle_reflection_limit_boundary line 39