case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
rcases h with ⟨⟨x, y⟩, hx, hy⟩
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
refine' ⟨fun hst => _, fun h => h.1.prod h.2⟩
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
have : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t) := measurable_prod_mk_right hst
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
this✝ : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
have : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t) := measurable_prod_mk_left hst
no goals
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.83086
δ : Type ?u.83089
δ' : Type ?u.83092
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
this✝ : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
simp_all