OAI/Analysis/CircleDomains/Probability/PolishProbabilityProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weak probability laws on a Polish space are Polish, with the measure-evaluation Borel structure. Embed the point space in the Hilbert cube; the laws supported on its G-delta image form a G-delta in the compact law space.

  1. lemma OAI.CircleDomainRigidity.polishProbabilityLaws line 18