OAI/Analysis/CircleDomains/Probability/FiniteMeasureCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Countably many measurable evaluations distinguish finite measures. Finite intersections of a generating sequence form the required pi system.

  1. def OAI.CircleDomainRigidity.measureCoordinateSet line 14
  2. lemma OAI.CircleDomainRigidity.measurableSet_measureCoordinateSet line 17
  3. lemma OAI.CircleDomainRigidity.measureCoordinateSet_union line 21
  4. lemma OAI.CircleDomainRigidity.measureCoordinateSet_generates line 27
  5. def OAI.CircleDomainRigidity.finiteMeasureCoordinates line 39
  6. lemma OAI.CircleDomainRigidity.measurable_finiteMeasureCoordinates line 42
  7. lemma OAI.CircleDomainRigidity.injective_finiteMeasureCoordinates line 48