case base
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t s : Set α
h_s : s ∈ S
⊢ MeasurableSet s

case inter
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty✝ : Set.Nonempty (s ∩ u)
h_s : MeasurableSet s
h_u : MeasurableSet u
⊢ MeasurableSet (s ∩ u)
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t : Set α
h_in_pi : t ∈ generatePiSystem S
⊢ MeasurableSet t
induction' h_in_pi with s h_s s u _ _ _ h_s h_u
no goals
case base
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t s : Set α
h_s : s ∈ S
⊢ MeasurableSet s
apply h_meas_S _ h_s
no goals
case inter
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty✝ : Set.Nonempty (s ∩ u)
h_s : MeasurableSet s
h_u : MeasurableSet u
⊢ MeasurableSet (s ∩ u)
apply MeasurableSet.inter h_s h_u