Mathlib Map

Structures · Topology

UniformSpace

A uniform space is a generalization of the "uniform" topological aspects of a metric space. It consists of a filter on α × α called the "uniformity", which satisfies properties analogous to the reflexivity, symmetry, and triangle properties of a metric. A metric space has a natural uniformity, and a uniform space has a natural topology. A topological group also has a natural uniformity, even when it is not metrizable.

Defined in
Mathlib.Topology.UniformSpace.Defs
Shape
One type argument · adds uniformity, symm, comp, nhds_eq_comap_uniformity
Open in Mathlib docs

Extends1

Extended by3

Forgetful instances

Provided automatically by

Concrete types that are instances50

  • Int
  • Nat
  • Bool
  • SeparationQuotient
  • ContinuousLinearMap
  • CStarMatrix
  • UniformSpace.Completion
  • Unitization
  • IsDedekindDomain.HeightOneSpectrum.adicCompletion
  • Matrix
  • WithLp
  • TrivSqZeroExt
  • UniformFun
  • UniformOnFun
  • ContinuousMapZero
  • ContinuousAlternatingMap
  • TopologicalSpace.NonemptyCompacts
  • ContinuousLinearMapWOT
  • WithCStarModule
  • CompareReals.Q
  • Empty
  • ContinuousMultilinearMap
  • SchwartzMap
  • TopologicalSpace.Compacts
  • PiLp
  • Circle
  • TestFunction
  • ContDiffMapSupportedIn
  • MvPolynomial
  • UniformConvergenceCLM
  • TopologicalSpace.Closeds
  • Path
  • Metric.Snowflaking
  • CauchyFilter
  • LaurentSeries
  • UniformSpaceCat.carrier
  • CpltSepUniformSpace.α
  • CompareReals.Bourbakiℝ
  • LaurentSeries.RatFuncAdicCompl
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • PUnit
  • AddOpposite
  • ContinuousMap
  • Sum
  • Multiplicative
  • Additive

How is a type an instance?

Loading the hierarchy index…

Assumed by2,238

Ancestors10