Theorems · Definition · general topology

Metric.IsCover

{X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → Set X → Prop

A set N is an `ε`-cover of a set s if every point of s lies at distance at most ε of some point of N. This is also called an `ε`-net in the literature. [R. Vershynin, High Dimensional Probability][vershynin2018high], 4.2.1.

Defined in

Mathlib.Topology.MetricSpace.Cover

Cited by

51 results in Mathlib

Foundations

Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace