HasBoundedInternalCoveringNumber #
def
HasBoundedInternalCoveringNumber
{T : Type u_1}
[PseudoEMetricSpace T]
(A : Set T)
(c : ENNReal)
(d : NNReal)
:
Equations
- HasBoundedInternalCoveringNumber A c d = ∀ ε ≤ EMetric.diam A, ↑(internalCoveringNumber ε A) ≤ c * ε⁻¹ ^ ↑d