α : Type u_2
α' : Type ?u.4446542
β : Type u_1
β' : Type ?u.4446548
γ : Type ?u.4446551
E : Type ?u.4446554
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (∫⁻ (x : α), ↑↑ν (Prod.mk x ⁻¹' s) ∂μ) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ↑↑ν (Prod.mk x ⁻¹' s) < ⊤
α : Type u_2
α' : Type ?u.4446542
β : Type u_1
β' : Type ?u.4446548
γ : Type ?u.4446551
E : Type ?u.4446554
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ ν) s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ↑↑ν (Prod.mk x ⁻¹' s) < ⊤
rw [prod_apply hs] at h2s
no goals
α : Type u_2
α' : Type ?u.4446542
β : Type u_1
β' : Type ?u.4446548
γ : Type ?u.4446551
E : Type ?u.4446554
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (∫⁻ (x : α), ↑↑ν (Prod.mk x ⁻¹' s) ∂μ) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ↑↑ν (Prod.mk x ⁻¹' s) < ⊤
refine' ae_lt_top (measurable_measure_prod_mk_left hs) h2s