ContinuousLawMeasurable.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Weakly continuous probability kernels are measurable for the evaluation sigma algebra. This follows from the open-set Portmanteau inequality and the pi-system of open sets.

theorem OAI.CircleDomainRigidity.measurable_of_continuous_probability line 15