case pos
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
hf : Integrable fun a => ↑(f a)
⊢ (∫ (a : α), ↑(f a) ∂μ) ≤ ↑b

case neg
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
hf : ¬Integrable fun a => ↑(f a)
⊢ (∫ (a : α), ↑(f a) ∂μ) ≤ ↑b
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
⊢ (∫ (a : α), ↑(f a) ∂μ) ≤ ↑b
by_cases hf : Integrable (fun a => (f a : ℝ)) μ
no goals
case pos
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
hf : Integrable fun a => ↑(f a)
⊢ (∫ (a : α), ↑(f a) ∂μ) ≤ ↑b
exact (lintegral_coe_le_coe_iff_integral_le hf).1 h
case neg
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
hf : ¬Integrable fun a => ↑(f a)
⊢ 0 ≤ ↑b
case neg
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
hf : ¬Integrable fun a => ↑(f a)
⊢ (∫ (a : α), ↑(f a) ∂μ) ≤ ↑b
rw [integral_undef hf]
no goals
case neg
α : Type u_1
E : Type ?u.1091665
F : Type ?u.1091668
𝕜 : Type ?u.1091671
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1094362
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
b : ℝ≥0
h : (∫⁻ (a : α), ↑(f a) ∂μ) ≤ ↑b
hf : ¬Integrable fun a => ↑(f a)
⊢ 0 ≤ ↑b
exact b.2