case hs₀
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hs₀ : ↑↑μ s ≠ 0
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ 0 < ENNReal.toReal (↑↑μ s)

α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hs₀ : ↑↑μ s ≠ 0
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
replace hs₀ : 0 < (μ s).toReal
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
case hs₀
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hs₀ : ↑↑μ s ≠ 0
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ 0 < ENNReal.toReal (↑↑μ s)

α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
exact ENNReal.toReal_pos hs₀ hsμ
case ht₀
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
⊢ 0 < ENNReal.toReal (↑↑μ t)

α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
ht₀ : 0 < ENNReal.toReal (↑↑μ t)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
replace ht₀ : 0 < (μ t).toReal
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
ht₀ : 0 < ENNReal.toReal (↑↑μ t)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
case ht₀
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
ht₀ : ↑↑μ t ≠ 0
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
⊢ 0 < ENNReal.toReal (↑↑μ t)

α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
ht₀ : 0 < ENNReal.toReal (↑↑μ t)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
exact ENNReal.toReal_pos ht₀ htμ
no goals
α : Type u_1
E : Type u_2
F : Type ?u.218635
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hs₀ : 0 < ENNReal.toReal (↑↑μ s)
ht₀ : 0 < ENNReal.toReal (↑↑μ t)
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
refine' mem_openSegment_iff_div.mpr
  ⟨(μ s).toReal, (μ t).toReal, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩