Theorems · Theorem · general topology

UniformSpace.comp

∀ {α : Type u} [self : UniformSpace α],
  (UniformSpace.uniformity.lift' fun s => SetRel.comp s s) ≤ UniformSpace.uniformity

For every set u ∈ uniformity, there exists v ∈ uniformity such that v ○ v ⊆ u.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

UniformSpace