case pos
α : Type u_1
β : Type ?u.3417223
E : Type u_2
F : Type ?u.3417229
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)

case neg
α : Type u_1
β : Type ?u.3417223
E : Type u_2
F : Type ?u.3417229
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
α : Type u_1
β : Type ?u.3417223
E : Type u_2
F : Type ?u.3417229
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
by_cases hab : a < b
no goals
case pos
α : Type u_1
β : Type ?u.3417223
E : Type u_2
F : Type ?u.3417229
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
rw [← Ioo_union_right hab, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true_iff]
no goals
case neg
α : Type u_1
β : Type ?u.3417223
E : Type u_2
F : Type ?u.3417229
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
rw [Ioo_eq_empty hab, Ioc_eq_empty hab]