case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ ∃ c, ∀ (x : Ω), ↑(↑f x) ≤ ↑c
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (ω : Ω), ↑(↑f ω) ∂μ) < ⊤
apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_eNNReal
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ ∀ (x : Ω), ↑(↑f x) ≤ ↑(nndist f 0)
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ ∃ c, ∀ (x : Ω), ↑(↑f x) ≤ ↑c
use nndist f 0
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
⊢ ↑(↑f x) ≤ ↑(nndist f 0)
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
⊢ ∀ (x : Ω), ↑(↑f x) ≤ ↑(nndist f 0)
intro x
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ ↑(↑f x) ≤ ↑(nndist f 0)
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
⊢ ↑(↑f x) ≤ ↑(nndist f 0)
have key := BoundedContinuousFunction.Nnreal.upper_bound f x
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ ↑(↑f x) ≤ ↑(nndist f 0)
rw [ENNReal.coe_le_coe]
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
eq : nndist f 0 = { val := dist f 0, property := (_ : 0 ≤ dist f 0) }
⊢ ↑f x ≤ nndist f 0
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ ↑f x ≤ nndist f 0
have eq : nndist f 0 = ⟨dist f 0, dist_nonneg⟩ := by
  ext
  simp only [Real.coe_toNNReal', max_eq_left_iff, NNReal.coe_mk, coe_nndist]
no goals
case f_bdd
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
eq : nndist f 0 = { val := dist f 0, property := (_ : 0 ≤ dist f 0) }
⊢ ↑f x ≤ nndist f 0
rwa [eq] at key
case a
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ ↑(nndist f 0) = ↑{ val := dist f 0, property := (_ : 0 ≤ dist f 0) }
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ nndist f 0 = { val := dist f 0, property := (_ : 0 ≤ dist f 0) }
ext
no goals
case a
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.44593
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ≥0
x : Ω
key : ↑f x ≤ nndist f 0
⊢ ↑(nndist f 0) = ↑{ val := dist f 0, property := (_ : 0 ≤ dist f 0) }
simp only [Real.coe_toNNReal', max_eq_left_iff, NNReal.coe_mk, coe_nndist]