α : Type u_1
E : Type u_2
F : Type ?u.9151247
G : Type ?u.9151250
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 μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖
α : Type u_1
E : Type u_2
F : Type ?u.9151247
G : Type ?u.9151250
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 μ
f : α →ᵇ E
⊢ ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p
refine' Lp.mem_Lp_of_ae_bound ‖f‖ _
case h
α : Type u_1
E : Type u_2
F : Type ?u.9151247
G : Type ?u.9151250
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 μ
f : α →ᵇ E
x : α
a✝ : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x
⊢ ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖
α : Type u_1
E : Type u_2
F : Type ?u.9151247
G : Type ?u.9151250
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 μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖
filter_upwards [f.toContinuousMap.coeFn_toAEEqFun μ] with x _
no goals
case h
α : Type u_1
E : Type u_2
F : Type ?u.9151247
G : Type ?u.9151250
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 μ
f : α →ᵇ E
x : α
a✝ : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x
⊢ ‖↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x‖ ≤ ‖f‖
convert f.norm_coe_le_norm x using 2