proximity generated by uniformity

Definition. Let $X$ be a uniform space with uniformity $𝒰$. The uniform proximity, or proximity generated by $\mathrm{U}$, is a binary relation $𝛿$ on the subsets of $X$, given by the formula

$$A𝛿B\mathit{\hspace{1em}\hspace{1em}}\iff \mathit{\hspace{1em}\hspace{1em}}\forall U\in 𝒰:U\cap (A\times B)\ne \mathrm{\varnothing }.$$

Correctness of the above proximity is given by the below theorem:

Theorem. Proximity generated by a uniformity is a proximity. In other words, $X$ is a proximity space with proximity $𝛿$.

Title	proximity generated by uniformity
Canonical name	ProximityGeneratedByUniformity
Date of creation	2013-03-22 16:56:20
Last modified on	2013-03-22 16:56:20
Owner	porton (9363)
Last modified by	porton (9363)
Numerical id	9
Author	porton (9363)
Entry type	Definition
Classification	msc 54E17
Classification	msc 54E15
Classification	msc 54E05
Defines	uniform proximity