case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ (t : Set α), t ∈ generatePiSystem g → MeasurableSet t

case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ (t : Set α), t ∈ g → MeasurableSet t
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) = generateFrom g
apply le_antisymm <;> apply generateFrom_le
no goals
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ (t : Set α), t ∈ generatePiSystem g → MeasurableSet t
exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t
no goals
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ (t : Set α), t ∈ g → MeasurableSet t
exact fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)