Documentation

Mathlib.Topology.UniformSpace.DiscreteUniformity

Discrete uniformity #

The discrete uniformity is the smallest possible uniformity, the one for which the diagonal is an entourage of itself.

It induces the discrete topology.

It is complete.

source
class DiscreteUniformity (X : Type u_1) [u : UniformSpace X] :
Prop

The discrete uniformity

Instances
    source
    theorem discreteUniformity_iff_eq_bot (X : Type u_1) [u : UniformSpace X] :
    DiscreteUniformity X ↔ u = ⊥
    source
    instance DiscreteUniformity.inst (X : Type u_1) :
    DiscreteUniformity X

    The bot uniformity is the discrete uniformity.

    source
    theorem discreteUniformity_iff_eq_principal_idRel {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ uniformity X = Filter.principal idRel
    source
    theorem DiscreteUniformity.eq_principal_idRel (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    uniformity X = Filter.principal idRel
    source
    instance DiscreteUniformity.instDiscreteTopology (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    DiscreteTopology X

    The discrete uniformity induces the discrete topology.

    source
    theorem discreteUniformity_iff_idRel_mem_uniformity {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ idRel ∈ uniformity X
    source
    theorem DiscreteUniformity.idRel_mem_uniformity (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    idRel ∈ uniformity X
    source
    instance DiscreteUniformity.instProd {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {Y : Type u_2} [UniformSpace Y] [DiscreteUniformity Y] :
    DiscreteUniformity (X × Y)

    A product of spaces with discrete uniformity has a discrete uniformity.

    source
    theorem DiscreteUniformity.uniformContinuous (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] {Y : Type u_2} [UniformSpace Y] (f : X → Y) :
    UniformContinuous f

    On a space with a discrete uniformity, any function is uniformly continuous.

    source
    instance DiscreteUniformity.instUniformGroup (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] [Group X] :
    UniformGroup X

    The discrete uniformity makes a group a `UniformGroup.

    source
    instance DiscreteUniformity.instUniformAddGroup (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] [AddGroup X] :
    UniformAddGroup X

    The discrete uniformity makes an additive group a UniformAddGroup.

    source
    theorem DiscreteUniformity.eq_pure_of_cauchy {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {α : Filter X} (hα : Cauchy α) :
    ∃ (x : X), α = pure x

    A Cauchy filter in a discrete uniform space is contained in the principal filter of a point.

    source
    @[deprecated DiscreteUniformity.eq_pure_of_cauchy (since := "2025-03-23")]
    theorem UniformSpace.DiscreteUnif.cauchy_le_pure {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {α : Filter X} (hα : Cauchy α) :
    ∃ (x : X), α = pure x

    Alias of DiscreteUniformity.eq_pure_of_cauchy.

    A Cauchy filter in a discrete uniform space is contained in the principal filter of a point.

    source
    instance DiscreteUniformity.instCompleteSpace (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    CompleteSpace X

    The discrete uniformity makes a space complete.

    source
    noncomputable def DiscreteUniformity.cauchyConst {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {α : Filter X} (hα : Cauchy α) :
    X

    A constant to which a Cauchy filter in a discrete uniform space converges.

    Equations
    Instances For
      source
      @[deprecated DiscreteUniformity.cauchyConst (since := "2025-03-23")]
      def UniformSpace.DiscreteUnif.cauchyConst {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {α : Filter X} (hα : Cauchy α) :
      X

      Alias of DiscreteUniformity.cauchyConst.

      A constant to which a Cauchy filter in a discrete uniform space converges.

      Equations
      Instances For
        source
        theorem DiscreteUniformity.eq_pure_cauchyConst {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {α : Filter X} (hα : Cauchy α) :
        α = pure (cauchyConst hα)
        source
        @[deprecated DiscreteUniformity.eq_pure_cauchyConst (since := "2025-03-23")]
        theorem UniformSpace.DiscreteUnif.eq_const_of_cauchy {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {α : Filter X} (hα : Cauchy α) :
        α = pure (DiscreteUniformity.cauchyConst hα)

        Alias of DiscreteUniformity.eq_pure_cauchyConst.