OAI/Analysis/CircleDomains/Probability/LocalPartialMeasurability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local L2 hypotheses supply global completed measurability of each weak partial.

  1. lemma OAI.CircleDomainRigidity.local_partial_aestronglyMeasurable line 11