theorem coveredByBalls_iff {X : Type u_1} [PseudoMetricSpace X] (s : Set X) (n : ℕ) (r : ℝ) : CoveredByBalls s n r ↔ ∃ (balls : Finset X), balls.card ≤ n ∧ s ⊆ ⋃ x ∈ balls, Metric.ball x r

class inductive CoveredByBalls {X : Type u_1} [PseudoMetricSpace X] (s : Set X) (n : ℕ) (r : ℝ) : Prop

s can be covered by at most N balls with radius r.

• mk: ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {s : Set X} {n : ℕ} {r : ℝ} (balls : Finset X), balls.card ≤ n → s ⊆ ⋃ x ∈ balls, Metric.ball x r → CoveredByBalls s n r

theorem CoveredByBalls.mono_set {X : Type u_1} [PseudoMetricSpace X] {s : Set X} {t : Set X} {n : ℕ} {r : ℝ} (h : CoveredByBalls t n r) (h2 : s ⊆ t) : CoveredByBalls s n r

theorem CoveredByBalls.mono_nat {X : Type u_1} [PseudoMetricSpace X] {s : Set X} {n : ℕ} {m : ℕ} {r : ℝ} (h : CoveredByBalls s n r) (h2 : n ≤ m) : CoveredByBalls s m r

theorem CoveredByBalls.mono_real {X : Type u_1} [PseudoMetricSpace X] {s : Set X} {n : ℕ} {r : ℝ} {r' : ℝ} (h : CoveredByBalls s n r) (h2 : r ≤ r') : CoveredByBalls s n r'

@[simp]

theorem CoveredByBalls.empty {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {r : ℝ} : CoveredByBalls ∅ n r

@[simp]

theorem CoveredByBalls.zero_left {X : Type u_1} [PseudoMetricSpace X] {s : Set X} {r : ℝ} : CoveredByBalls s 0 r ↔ s = ∅

@[simp]

theorem CoveredByBalls.zero_right {X : Type u_1} [PseudoMetricSpace X] {s : Set X} {n : ℕ} : CoveredByBalls s n 0 ↔ s = ∅

def BallsCoverBalls (X : Type u_1) [PseudoMetricSpace X] (r : ℝ) (r' : ℝ) (n : ℕ) : Prop

Balls of radius r in are covered by n balls of radius r'

Equations

• BallsCoverBalls X r r' n = ∀ (x : X), CoveredByBalls (Metric.ball x r) n r'

theorem CoveredByBalls.trans {X : Type u_1} [PseudoMetricSpace X] {s : Set X} {n : ℕ} {m : ℕ} {r : ℝ} {r' : ℝ} (h : CoveredByBalls s n r) (h2 : BallsCoverBalls X r r' m) : CoveredByBalls s (n * m) r'

theorem BallsCoverBalls.trans {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {m : ℕ} {r₁ : ℝ} {r₂ : ℝ} {r₃ : ℝ} (h1 : BallsCoverBalls X r₁ r₂ n) (h2 : BallsCoverBalls X r₂ r₃ m) : BallsCoverBalls X r₁ r₃ (n * m)

theorem BallCoversSelf {X : Type u_1} [PseudoMetricSpace X] (x : X) (r : ℝ) : CoveredByBalls (Metric.ball x r) 1 r

theorem BallsCoverBalls.pow_mul {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {r : ℝ} {a : ℝ} {k : ℕ} (h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n) : BallsCoverBalls X (a ^ k * r) r (n ^ k)

theorem BallsCoverBalls.pow {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {a : ℝ} {k : ℕ} (h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n) : BallsCoverBalls X (a ^ k) 1 (n ^ k)