α : Type ?u.1725284
E : Type ?u.1725287
F : Type ?u.1725290
𝕜 : Type ?u.1725293
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
H : Type ?u.1727964
β : Type u_2
γ : Type u_1
inst✝² : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
inst✝¹ : TopologicalSpace γ
inst✝ : MetrizableSpace γ
hm : m ≤ m0
f g : β → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
α : Type ?u.1725284
E : Type ?u.1725287
F : Type ?u.1725290
𝕜 : Type ?u.1725293
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
H : Type ?u.1727964
β : Type u_2
γ : Type u_1
inst✝² : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
inst✝¹ : TopologicalSpace γ
inst✝ : MetrizableSpace γ
hm : m ≤ m0
f g : β → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ f =ᵐ[Measure.trim μ hm] g
rwa [EventuallyEq, @ae_iff _ m, trim_measurableSet_eq hm _]
no goals
α : Type ?u.1725284
E : Type ?u.1725287
F : Type ?u.1725290
𝕜 : Type ?u.1725293
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
H : Type ?u.1727964
β : Type u_2
γ : Type u_1
inst✝² : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
inst✝¹ : TopologicalSpace γ
inst✝ : MetrizableSpace γ
hm : m ≤ m0
f g : β → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
exact (hf.measurableSet_eq_fun hg).compl