OAI/Analysis/CircleDomains/Probability/ArcImageMeasures.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Disjoint portions of a simple arc have disjoint image measures after their shared endpoints, which have zero Hausdorff length, are removed.

  1. theorem OAI.CircleDomainRigidity.arc_image_Icc_ae_eq_Ioc line 14
  2. theorem OAI.CircleDomainRigidity.sum_disjoint_arc_image_measures_le line 27