Theorem: CoveredByBalls.empty (Carleson/CoverByBalls.lean)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ ∅.card ≤ n
Tactic:
simp
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ ∅ ⊆ ⋃ x ∈ ∅, ball x r
Tactic:
simp
State after:
no goals