α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
⊢ f = g
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g ↔ f = g
refine' ⟨fun h => _, by tauto⟩
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
⊢ ↑f =ᵐ[μ] ↑g
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
⊢ f = g
rw [← FunLike.coe_fn_eq, ← (map_continuous f).ae_eq_iff_eq μ (map_continuous g)]
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
⊢ ↑↑(↑(toLp p μ 𝕜) f) =ᵐ[μ] ↑↑(↑(toLp p μ 𝕜) g)
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
⊢ ↑f =ᵐ[μ] ↑g
refine' (coeFn_toLp p μ 𝕜 f).symm.trans (EventuallyEq.trans _ <| coeFn_toLp p μ 𝕜 g)
no goals
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
⊢ ↑↑(↑(toLp p μ 𝕜) f) =ᵐ[μ] ↑↑(↑(toLp p μ 𝕜) g)
rw [h]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.12183215
G : Type ?u.12183218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ f = g → ↑(toLp p μ 𝕜) f = ↑(toLp p μ 𝕜) g
tauto