α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ↑↑ν (Prod.mk x ⁻¹' s)
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ↑↑ν (Prod.mk x ⁻¹' s)
have : ∀ x, MeasurableSet (Prod.mk x ⁻¹' s) := fun x => measurable_prod_mk_left hs
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ⨆ (i : ℕ), ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk x ⁻¹' s)
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ↑↑ν (Prod.mk x ⁻¹' s)
simp only [← @iSup_restrict_spanningSets _ _ ν, this]
case hf
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∀ (i : ℕ), Measurable fun b => ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk b ⁻¹' s)
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ⨆ (i : ℕ), ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk x ⁻¹' s)
apply measurable_iSup
case hf
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
i : ℕ
⊢ Measurable fun b => ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk b ⁻¹' s)
case hf
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∀ (i : ℕ), Measurable fun b => ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk b ⁻¹' s)
intro i
case hf
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this✝ : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
i : ℕ
this : Fact (↑↑ν (spanningSets ν i) < ⊤)
⊢ Measurable fun b => ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk b ⁻¹' s)
case hf
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
i : ℕ
⊢ Measurable fun b => ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk b ⁻¹' s)
haveI := Fact.mk (measure_spanningSets_lt_top ν i)
no goals
case hf
α : Type u_2
α' : Type ?u.1887086
β : Type u_1
β' : Type ?u.1887092
γ : Type ?u.1887095
E : Type ?u.1887098
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
this✝ : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
i : ℕ
this : Fact (↑↑ν (spanningSets ν i) < ⊤)
⊢ Measurable fun b => ↑↑(Measure.restrict ν (spanningSets ν i)) (Prod.mk b ⁻¹' s)
exact measurable_measure_prod_mk_left_finite hs