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

State before:
X : Type
inst✝ : PseudoMetricSpace X
f g : C(X, ℂ)
⊢ localOscillation ∅ f g = 0
Tactic:
simp [localOscillation]
State after:
no goals