α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)
α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace
      (toMeasurableSpace (generate s)
        (_ : ∀ (t₁ t₂ : Set α), Has (generate s) t₁ → Has (generate s) t₂ → Has (generate s) (t₁ ∩ t₂))) ≤
    ofMeasurableSpace (generateFrom s)
rw [ofMeasurableSpace_toMeasurableSpace]
no goals
α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)
exact generate_le _ fun t ht => measurableSet_generateFrom ht