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

case neg
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
by_cases hab : a ≤ b
no goals
case pos
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
rw [← Ioc_union_left hab, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr ha.lt_top), and_true_iff]
case neg
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b
case neg
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
rw [Icc_eq_empty hab, Ioc_eq_empty]
case neg
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : a < b
⊢ a ≤ b
case neg
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b
contrapose! hab
no goals
case neg
α : Type u_1
β : Type ?u.3069209
E : Type u_2
F : Type ?u.3069215
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : a < b
⊢ a ≤ b
exact hab.le