OAI/Analysis/CircleDomains/Probability/StandardBorelProbabilityProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Probability laws on a standard Borel space are standard Borel. Embed the point space into Cantor space and identify the image of the induced map on laws by its measurable support condition.

  1. lemma OAI.CircleDomainRigidity.standardBorelProbabilityLaws line 15