no goals
α : Type u_1
E : Type ?u.116296
F : Type u_2
𝕜 : Type ?u.116302
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.116404
F' : Type ?u.116407
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = ENNReal.toReal (↑↑μ Set.univ) • y
classical
calc
  (const α y).integral μ = ∑ z in {y}, (μ (const α y ⁻¹' {z})).toReal • z :=
    integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
  _ = (μ univ).toReal • y := by simp [Set.preimage]
no goals
α : Type u_1
E : Type ?u.116296
F : Type u_2
𝕜 : Type ?u.116302
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.116404
F' : Type ?u.116407
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = ENNReal.toReal (↑↑μ Set.univ) • y
calc
  (const α y).integral μ = ∑ z in {y}, (μ (const α y ⁻¹' {z})).toReal • z :=
    integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
  _ = (μ univ).toReal • y := by simp [Set.preimage]
no goals
α : Type u_1
E : Type ?u.116296
F : Type u_2
𝕜 : Type ?u.116302
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.116404
F' : Type ?u.116407
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
y : F
⊢ ∑ z in {y}, ENNReal.toReal (↑↑μ (↑(const α y) ⁻¹' {z})) • z = ENNReal.toReal (↑↑μ Set.univ) • y
simp [Set.preimage]