α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
⊢ IntegrableOn f {x} ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
⊢ IntegrableOn f {x} ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
have : f =ᵐ[μ.restrict {x}] fun _ => f x := by
  filter_upwards [ae_restrict_mem (measurableSet_singleton x)]with _ ha
  simp only [mem_singleton_iff.1 ha]
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
⊢ f x = 0 ∨ ↑↑(Measure.restrict μ {x}) univ < ⊤ ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
⊢ IntegrableOn f {x} ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
rw [IntegrableOn, integrable_congr this, integrable_const_iff]
no goals
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
⊢ f x = 0 ∨ ↑↑(Measure.restrict μ {x}) univ < ⊤ ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
simp
case h
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
a✝ : α
ha : a✝ ∈ {x}
⊢ f a✝ = f x
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
⊢ f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
filter_upwards [ae_restrict_mem (measurableSet_singleton x)]with _ ha
no goals
case h
α : Type u_1
β : Type ?u.1501840
E : Type u_2
F : Type ?u.1501846
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
a✝ : α
ha : a✝ ∈ {x}
⊢ f a✝ = f x
simp only [mem_singleton_iff.1 ha]