Theorem: localOscillation_on_empty_ball (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
X : Type
inst✝ : PseudoMetricSpace X
x : X
f g : C(X, ℂ)
R : ℝ
R_nonpos : R ≤ 0
⊢ localOscillation (Metric.ball x R) f g = 0
Tactic:
convert localOscillation_on_emptyset
State after:
case h.e'_2.h.e'_3
X : Type
inst✝ : PseudoMetricSpace X
x : X
f g : C(X, ℂ)
R : ℝ
R_nonpos : R ≤ 0
⊢ Metric.ball x R = ∅

State before:
case h.e'_2.h.e'_3
X : Type
inst✝ : PseudoMetricSpace X
x : X
f g : C(X, ℂ)
R : ℝ
R_nonpos : R ≤ 0
⊢ Metric.ball x R = ∅
Tactic:
exact Metric.ball_eq_empty.mpr R_nonpos
State after:
no goals