OAI/Analysis/CircleDomains/Modulus/SimpleArcLength.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The variation of an injective arc is paid by the Hausdorff length of its image. Disjoint parameter intervals have disjoint half-open images.

  1. theorem OAI.CircleDomainRigidity.simple_arc_edist_le_length_Ioc line 15
  2. theorem OAI.CircleDomainRigidity.simple_arc_variation_le_length line 41