# HasBoundedInternalCoveringNumber #

source
def HasBoundedInternalCoveringNumber {T : Type u_1} [PseudoEMetricSpace T] (A : Set T) (c : ENNReal) (d : ℝ) :
Prop
Equations

- HasBoundedInternalCoveringNumber A c d = ∀ ε ≤ EMetric.diam A, ↑(internalCoveringNumber ε A) ≤ c * ε⁻¹ ^ d

Instances For

source
theorem HasBoundedInternalCoveringNumber.internalCoveringNumber_lt_top {T : Type u_1} [PseudoEMetricSpace T] {A : Set T} {c ε : ENNReal} {d : ℝ} (h : HasBoundedInternalCoveringNumber A c d) (hε_ne : ε ≠ 0) (hc : c ≠ ⊤) (hd : 0 ≤ d) :
internalCoveringNumber ε A < ⊤
source
theorem HasBoundedInternalCoveringNumber.diam_lt_top {T : Type u_1} [PseudoEMetricSpace T] {A : Set T} {c : ENNReal} {d : ℝ} (h : HasBoundedInternalCoveringNumber A c d) (hd : 0 < d) :
EMetric.diam A < ⊤
source
theorem HasBoundedInternalCoveringNumber.subset {T : Type u_1} [PseudoEMetricSpace T] {A : Set T} {c : ENNReal} {d : ℝ} {B : Set T} (h : HasBoundedInternalCoveringNumber A c d) (hBA : B ⊆ A) (hd : 0 ≤ d) :
HasBoundedInternalCoveringNumber B (2 ^ d * c) d
source
structure IsCoverWithBoundedCoveringNumber {T : Type u_1} [PseudoEMetricSpace T] (C : ℕ → Set T) (A : Set T) (c : ℕ → ENNReal) (d : ℕ → ℝ) :
Prop

- c_ne_top (n : ℕ) : c n ≠ ⊤
- d_pos (n : ℕ) : 0 < d n
- isOpen (n : ℕ) : IsOpen (C n)
- totallyBounded (n : ℕ) : TotallyBounded (C n)
- hasBoundedCoveringNumber (n : ℕ) : HasBoundedInternalCoveringNumber (C n) (c n) (d n)
- mono (n m : ℕ) : n ≤ m → C n ⊆ C m
- subset_iUnion : A ⊆ ⋃ (i : ℕ), C i

Instances For

source
theorem isCoverWithBoundedCoveringNumber_Ico_nnreal :
IsCoverWithBoundedCoveringNumber (fun (n : ℕ) => Set.Ico 0 (↑n + 1)) Set.univ (fun (n : ℕ) => 3 * (↑n + 1)) fun (x : ℕ) => 1