simp
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ MeasurableSet {a}
no goals