α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ ∀ (t : Set α), t ∈ piiUnionInter π S → MeasurableSet t
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m
refine' generateFrom_le _
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ (x : ι), x ∈ ht_p → ft x ∈ π x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ ht_p), ft x)
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ ∀ (t : Set α), t ∈ piiUnionInter π S → MeasurableSet t
rintro t ⟨ht_p, _, ft, hft_mem_pi, rfl⟩
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ (x : ι), x ∈ ht_p → ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ (x : ι), x ∈ ht_p → ft x ∈ π x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ ht_p), ft x)
refine' Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ _
no goals
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ (x : ι), x ∈ ht_p → ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)
exact measurableSet_generateFrom (hft_mem_pi x hx_mem)