OAI/Analysis/CircleDomains/Probability/MeasurableBaireBranch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A measurable least-child choice constructs a Baire branch when each finite-prefix membership set is measurable for the completed measure.

  1. theorem OAI.CircleDomainRigidity.exists_nullMeasurable_baire_branch line 12