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_relId {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ uniformity X = Filter.principal SetRel.id
    source
    @[deprecated discreteUniformity_iff_eq_principal_relId (since := "2025-10-17")]
    theorem DiscreteUniformity.discreteUniformity_iff_eq_principal_idRel {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ uniformity X = Filter.principal SetRel.id

    Alias of discreteUniformity_iff_eq_principal_relId.

    source
    theorem DiscreteUniformity.eq_principal_relId (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    uniformity X = Filter.principal SetRel.id
    source
    @[deprecated DiscreteUniformity.eq_principal_relId (since := "2025-10-17")]
    theorem DiscreteUniformity.eq_principal_idRel (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    uniformity X = Filter.principal SetRel.id

    Alias of DiscreteUniformity.eq_principal_relId.

    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_relId_mem_uniformity {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ SetRel.id ∈ uniformity X
    source
    @[deprecated discreteUniformity_iff_relId_mem_uniformity (since := "2025-10-17")]
    theorem DiscreteUniformity.discreteUniformity_iff_idRel_mem_uniformity {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ SetRel.id ∈ uniformity X

    Alias of discreteUniformity_iff_relId_mem_uniformity.

    source
    theorem DiscreteUniformity.relId_mem_uniformity (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    SetRel.id ∈ uniformity X
    source
    @[deprecated DiscreteUniformity.relId_mem_uniformity (since := "2025-10-17")]
    theorem DiscreteUniformity.idRel_mem_uniformity (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    SetRel.id ∈ uniformity X

    Alias of DiscreteUniformity.relId_mem_uniformity.

    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.