case intro.intro.intro
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : ↑↑(Measure.prod μ ν) t = 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
case intro.intro.intro
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ↑↑ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
case intro.intro.intro
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : ↑↑(Measure.prod μ ν) t = 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
rw [measure_prod_null mt] at ht
case intro.intro.intro
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ↑↑ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) ≤ᶠ[ae μ] 0 ∧ 0 ≤ᶠ[ae μ] fun x => ↑↑ν (Prod.mk x ⁻¹' s)
case intro.intro.intro
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ↑↑ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
rw [eventuallyLE_antisymm_iff]
no goals
case intro.intro.intro
α : Type u_2
α' : Type ?u.4447841
β : Type u_1
β' : Type ?u.4447847
γ : Type ?u.4447850
E : Type ?u.4447853
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
h : ↑↑(Measure.prod μ ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ↑↑ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) ≤ᶠ[ae μ] 0 ∧ 0 ≤ᶠ[ae μ] fun x => ↑↑ν (Prod.mk x ⁻¹' s)
exact
  ⟨EventuallyLE.trans_eq (eventually_of_forall fun x => (measure_mono (preimage_mono hst) : _))
      ht,
    eventually_of_forall fun x => zero_le _⟩