no goals
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
h : Set.Nonempty (Set.pi s t)
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
classical
  rcases h with ⟨f, hf⟩
  refine' ⟨fun hst i hi => _, MeasurableSet.pi hs⟩
  convert measurable_update f (a := i) hst
  rw [update_preimage_pi hi]
  exact fun j hj _ => hf j hj
case intro
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
h : Set.Nonempty (Set.pi s t)
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
rcases h with ⟨f, hf⟩
case intro
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (t i)
case intro
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
refine' ⟨fun hst i hi => _, MeasurableSet.pi hs⟩
case h.e'_3
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ t i = update f i ⁻¹' Set.pi s t
case intro
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (t i)
convert measurable_update f (a := i) hst
case h.e'_3
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ ∀ (j : δ), j ∈ s → j ≠ i → f j ∈ t j
case h.e'_3
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ t i = update f i ⁻¹' Set.pi s t
rw [update_preimage_pi hi]
no goals
case h.e'_3
α : Type ?u.147740
β : Type ?u.147743
γ : Type ?u.147746
δ : Type u_1
δ' : Type ?u.147752
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ ∀ (j : δ), j ∈ s → j ≠ i → f j ∈ t j
exact fun j hj _ => hf j hj