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} [PseudoMetricSpace X] {s : Set X} {n : ℕ} {r : ℝ} (balls : Finset X) (card_balls : balls.card ≤ n) (union_balls : s ⊆ ⋃ x ∈ balls, Metric.ball x r) : CoveredByBalls s n r

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

theorem CoveredByBalls.mono_set {X : Type u_1} [PseudoMetricSpace X] {s 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 = ∅

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

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

Balls of radius r in X 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.mono {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {r₁ r₂ r₃ : ℝ} (h : BallsCoverBalls X r₂ r₃ n) (h2 : r₁ ≤ r₂) : BallsCoverBalls X r₁ r₃ n

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 BallsCoverBalls.zero {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {r : ℝ} : BallsCoverBalls X 0 r n

theorem BallsCoverBalls.nonpos {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {r r' : ℝ} (hr' : r' ≤ 0) : BallsCoverBalls X r' r n

def AllBallsCoverBalls (X : Type u_1) [PseudoMetricSpace X] (a : ℝ) (n : ℕ) : Prop

For all r, balls of radius r in X are covered by n balls of radius a * r

Equations

• AllBallsCoverBalls X a n = ∀ (r : ℝ), BallsCoverBalls X (a * r) r n

theorem AllBallsCoverBalls.mk {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {a : ℝ} (ha : 0 ≤ a) (h : ∀ r > 0, BallsCoverBalls X (a * r) r n) : AllBallsCoverBalls X a n

Prove AllBallsCoverBalls only for balls of positive radius.

theorem AllBallsCoverBalls.pow {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {a : ℝ} {k : ℕ} (h : AllBallsCoverBalls X a n) : AllBallsCoverBalls X (a ^ k) (n ^ k)

theorem AllBallsCoverBalls.ballsCoverBalls_pow {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {a : ℝ} {k : ℕ} (h : AllBallsCoverBalls X a n) : BallsCoverBalls X (a ^ k) 1 (n ^ k)

theorem AllBallsCoverBalls.ballsCoverBalls {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {r r' a : ℝ} (h : AllBallsCoverBalls X a n) (h2 : 1 < a) (hr : 0 < r) : BallsCoverBalls X r' r (n ^ ⌈Real.logb a (r' / r)⌉₊)

theorem Metric.secondCountableTopology_of_almost_dense_set_balls_nat {α : Type u_2} [PseudoMetricSpace α] (x₀ : α) (H : ∀ ε > 0, ∀ (n : ℕ), ∃ (s : Set α), s.Countable ∧ ∀ x ∈ ball x₀ ↑n, ∃ y ∈ s, dist x y ≤ ε) : SecondCountableTopology α

A pseudometric space is second countable if, for every ε > 0 and every ball B with natural number radius around a given point x₀, there is a countable set which is ε-dense in B.

theorem Metric.secondCountableTopology_of_almost_dense_set_balls {α : Type u_2} [PseudoMetricSpace α] (H : ∀ (x₀ : α), ∀ ε > 0, ∀ (r : ℝ), ∃ (s : Set α), s.Countable ∧ ∀ x ∈ ball x₀ r, ∃ y ∈ s, dist x y ≤ ε) : SecondCountableTopology α

A pseudometric space is second countable if, for every ε > 0 and every ball B, there is a countable set which is ε-dense in B.

theorem BallsCoverBalls.secondCountableTopology {X : Type u_1} [PseudoMetricSpace X] (H : ∀ ε > 0, ∀ (r : ℝ), ∃ (n : ℕ), BallsCoverBalls X r ε n) : SecondCountableTopology X

A pseudometric space is second countable if, for every ε > 0 and every ball B is covered by finitely many balls of radius ε.

theorem AllBallsCoverBalls.secondCountableTopology {X : Type u_1} [PseudoMetricSpace X] {n : ℕ} {a : ℝ} (h : AllBallsCoverBalls X a n) (h2 : 1 < a) : SecondCountableTopology X

A pseudometric space is second countable if every ball of radius a * r is covered by b many balls of radius r.