Covers by sets with bounded covering exponent

theorem Metric.HasCoveringExponent.ediam_le {T : Type u_1} [PseudoEMetricSpace T] {A : Set T} {c : ENNReal} {d : ℝ} (h : HasCoveringExponent A c d) (hd : 0 < d) : ediam A ≤ c ^ d⁻¹

The covering condition at scale diam A bounds the diameter of A by c ^ (1/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
• isOpen (n : ℕ) : IsOpen (C n)
• totallyBounded (n : ℕ) : TotallyBounded (C n)
• hasBoundedCoveringNumber (n : ℕ) : Metric.HasCoveringExponent (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 : ℕ) => 3 * (↑n + 1)) fun (x : ℕ) => 1