Theorems · Definition · general topology

SetRel.IsCover

{X : Type u_1} → SetRel X X → Set X → Set X → Prop

For an entourage U, a set N is a `U`-cover of a set s if every point of s is U-close to some point of N. This is also called a `U`-net in the literature. [R. Vershynin, High Dimensional Probability][vershynin2018high], 4.2.1.

Defined in

Mathlib.Data.Rel.Cover

Cited by

17 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms