OAI/Analysis/CircleDomains/Probability/CompactFiniteMeasureBorel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact families of finite measures retain their original evaluation sigma algebra. A countable continuous and measurable code proves both compact-set measurability and the Borel structure on each compact family.

  1. lemma OAI.CircleDomainRigidity.exists_finiteMeasure_countable_code line 15
  2. lemma OAI.CircleDomainRigidity.compact_finiteMeasure_measurableSet line 53
  3. lemma OAI.CircleDomainRigidity.compact_finiteMeasure_borel line 62
  4. lemma OAI.CircleDomainRigidity.compact_finiteMeasure_polish line 75