equivalent condition for being a fundamental system of entourages


Lemma.

Let X be a set and let B be a nonempty family of subsets of X×X. Then B is a fundamental system of entourages of a uniformity on X if and only if it satisfies the following axioms.

  • (B1) If S, T, then ST contains an element of .

  • (B2) Each element of contains the diagonal Δ(X).

  • (B3) For any S, the inverse relation of S contains an element of .

  • (B4) For any S, there is an element T such that the relational compositionPlanetmathPlanetmath TT is contained in S.

Proof.

Suppose is a fundamental system of entourages for a uniformity 𝒰. Verification of axiom (B2) is immediate, since 𝒰 and each entourage is already required to contain the diagonal of X. We will prove that satisfies (B1); the proofs that (B3) and (B4) hold are analogous.

Let S, T be entourages in 𝒰. Since 𝒰 is closed underPlanetmathPlanetmath binary intersectionsMathworldPlanetmath, ST𝒰. By the definition of fundamental system of entourages, since ST𝒰, there exists an entourage B such that BST. Thus satisfies axioms (B1) through (B4).

To prove the converseMathworldPlanetmath, define a family of subsets of X×X by

𝒰={SX×X:BS for some B}.

By construction, each element of 𝒰 contains an element of , so all that remains is to show that 𝒰 is a uniformity. Suppose T is a subset of X×X that contains an element S𝒰. By the definition of 𝒰, there exists some B such that BS. Since ST, it follows that BT, so T satisfies the requirement for membership in 𝒰. Thus 𝒰 is closed under taking supersets. The remaining axioms for a uniformity follow directly from the appropriate axioms for the fundamental system of entourages by applying the axiom we have just checked. Hence is a fundamental system of entourages for a uniformity on X. ∎

Title equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath condition for being a fundamental system of entourages
Canonical name EquivalentConditionForBeingAFundamentalSystemOfEntourages
Date of creation 2013-03-22 16:30:02
Last modified on 2013-03-22 16:30:02
Owner mps (409)
Last modified by mps (409)
Numerical id 5
Author mps (409)
Entry type Derivation
Classification msc 54E15