α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.64507
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ↑(pair f g) ⁻¹' {b} ×ˢ {c} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.64507
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ↑(pair f g) ⁻¹' {(b, c)} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
rw [← singleton_prod_singleton]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.64507
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ↑(pair f g) ⁻¹' {b} ×ˢ {c} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
exact pair_preimage _ _ _ _