α : Type u_2
E : Type u_1
F : Type ?u.367774
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
hs : Convex ℝ s
hsc : IsClosed s
h0 : ↑↑μ t ≠ 0
ht : ↑↑μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x ∈ s
hfi : IntegrableOn f t
this : Fact (↑↑μ t < ⊤)
⊢ (⨍ (x : α) in t, f x ∂μ) ∈ s
α : Type u_2
E : Type u_1
F : Type ?u.367774
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
hs : Convex ℝ s
hsc : IsClosed s
h0 : ↑↑μ t ≠ 0
ht : ↑↑μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x ∈ s
hfi : IntegrableOn f t
⊢ (⨍ (x : α) in t, f x ∂μ) ∈ s
haveI : Fact (μ t < ∞) := ⟨ht.lt_top⟩
α : Type u_2
E : Type u_1
F : Type ?u.367774
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
hs : Convex ℝ s
hsc : IsClosed s
h0 : ↑↑μ t ≠ 0
ht : ↑↑μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x ∈ s
hfi : IntegrableOn f t
this : Fact (↑↑μ t < ⊤)
⊢ Measure.restrict μ t ≠ 0
α : Type u_2
E : Type u_1
F : Type ?u.367774
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
hs : Convex ℝ s
hsc : IsClosed s
h0 : ↑↑μ t ≠ 0
ht : ↑↑μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x ∈ s
hfi : IntegrableOn f t
this : Fact (↑↑μ t < ⊤)
⊢ (⨍ (x : α) in t, f x ∂μ) ∈ s
refine' hs.average_mem hsc _ hfs hfi
no goals
α : Type u_2
E : Type u_1
F : Type ?u.367774
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
hs : Convex ℝ s
hsc : IsClosed s
h0 : ↑↑μ t ≠ 0
ht : ↑↑μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x ∈ s
hfi : IntegrableOn f t
this : Fact (↑↑μ t < ⊤)
⊢ Measure.restrict μ t ≠ 0
rwa [Ne.def, restrict_eq_zero]