HasBoundedInternalCoveringNumber

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

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 < ⊤

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 < ⊤

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

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
• 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

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