English
Applying ofMeasurableSpace to the MeasurableSpace obtained from a Dynkin system yields back the original Dynkin system.
Русский
Применение ofMeasurableSpace к полученной σ‑алгебре возвращает исходную Dynkin‑систему.
LaTeX
$$$\mathrm{ofMeasurableSpace}(\mathrm{toMeasurableSpace}(d)) = d$$$
Lean4
/-- If a Dynkin system is closed under binary intersection, then it forms a `σ`-algebra. -/
def toMeasurableSpace (h_inter : ∀ s₁ s₂, d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)) : MeasurableSpace α
where
MeasurableSet' := d.Has
measurableSet_empty := d.has_empty
measurableSet_compl _ h := d.has_compl h
measurableSet_iUnion f
hf := by
rw [← iUnion_disjointed]
exact
d.has_iUnion (disjoint_disjointed _) fun n =>
disjointedRec (fun (t : Set α) i h => h_inter _ _ h <| d.has_compl <| hf i) (hf n)
