no goals
α✝ : Type ?u.46613
β : Type ?u.46616
E : Type ?u.46619
F : Type ?u.46622
inst✝³ : MeasurableSpace α✝
inst✝² : NormedAddCommGroup E
f g : α✝ → E
s✝ t : Set α✝
μ✝ ν : Measure α✝
l l' : Filter α✝
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
⊢ ENNReal.ofReal (∫ (x : α) in s, 1 ∂μ) = ENNReal.ofReal (∫ (x : α) in s, ‖1‖ ∂μ)
simp only [norm_one]
α✝ : Type ?u.46613
β : Type ?u.46616
E : Type ?u.46619
F : Type ?u.46622
inst✝³ : MeasurableSpace α✝
inst✝² : NormedAddCommGroup E
f g : α✝ → E
s✝ t : Set α✝
μ✝ ν : Measure α✝
l l' : Filter α✝
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
⊢ (∫⁻ (x : α) in s, ↑‖1‖₊ ∂μ) = ∫⁻ (x : α) in s, 1 ∂μ
α✝ : Type ?u.46613
β : Type ?u.46616
E : Type ?u.46619
F : Type ?u.46622
inst✝³ : MeasurableSpace α✝
inst✝² : NormedAddCommGroup E
f g : α✝ → E
s✝ t : Set α✝
μ✝ ν : Measure α✝
l l' : Filter α✝
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
⊢ ENNReal.ofReal (∫ (x : α) in s, ‖1‖ ∂μ) = ∫⁻ (x : α) in s, 1 ∂μ
rw [ofReal_integral_norm_eq_lintegral_nnnorm (integrableOn_const.2 (Or.inr hs.lt_top))]
no goals
α✝ : Type ?u.46613
β : Type ?u.46616
E : Type ?u.46619
F : Type ?u.46622
inst✝³ : MeasurableSpace α✝
inst✝² : NormedAddCommGroup E
f g : α✝ → E
s✝ t : Set α✝
μ✝ ν : Measure α✝
l l' : Filter α✝
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
⊢ (∫⁻ (x : α) in s, ↑‖1‖₊ ∂μ) = ∫⁻ (x : α) in s, 1 ∂μ
simp only [nnnorm_one, ENNReal.coe_one]