α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
⊢ MeasurableSet (f ⁻¹' s)
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)
have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ ({y} : Set β) := by
  ext1 ⟨x, y⟩
  simp [and_assoc, and_left_comm]
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
⊢ MeasurableSet (⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y})
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
⊢ MeasurableSet (f ⁻¹' s)
rw [this]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
⊢ MeasurableSet (⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y})
exact .iUnion fun y => (hf y hs).prod (.singleton y)
case h.mk
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
ext1 ⟨x, y⟩
no goals
case h.mk
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.86341
δ' : Type ?u.86344
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
simp [and_assoc, and_left_comm]