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
🔶 coverage
class DiscreteUniformity (X : Type u_1) [u : UniformSpace X] :
Prop

The discrete uniformity

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

    The bot uniformity is the discrete uniformity.

    source
    📐 coverage
    theorem discreteUniformity_iff_eq_principal_setRelId {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ uniformity X = Filter.principal SetRel.id
    source
    📐 coverage
    @[deprecated discreteUniformity_iff_eq_principal_setRelId (since := "2025-12-19")]
    theorem discreteUniformity_iff_eq_principal_relId {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ uniformity X = Filter.principal SetRel.id

    Alias of discreteUniformity_iff_eq_principal_setRelId.

    source
    📐 coverage
    @[deprecated discreteUniformity_iff_eq_principal_setRelId (since := "2025-10-17")]
    theorem 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_setRelId.

    source
    📐 coverage
    theorem DiscreteUniformity.eq_principal_setRelId (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    uniformity X = Filter.principal SetRel.id
    source
    📐 coverage
    @[deprecated DiscreteUniformity.eq_principal_setRelId (since := "2025-12-19")]
    theorem DiscreteUniformity.eq_principal_relId (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    uniformity X = Filter.principal SetRel.id

    Alias of DiscreteUniformity.eq_principal_setRelId.

    source
    📐 coverage
    @[deprecated DiscreteUniformity.eq_principal_setRelId (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_setRelId.

    source
    📐 coverage
    instance DiscreteUniformity.instDiscreteTopology (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    DiscreteTopology X

    The discrete uniformity induces the discrete topology.

    source
    📐 coverage
    theorem discreteUniformity_iff_setRelId_mem_uniformity {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ SetRel.id ∈ uniformity X
    source
    📐 coverage
    @[deprecated discreteUniformity_iff_setRelId_mem_uniformity (since := "2025-12-19")]
    theorem discreteUniformity_iff_relId_mem_uniformity {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ SetRel.id ∈ uniformity X

    Alias of discreteUniformity_iff_setRelId_mem_uniformity.

    source
    📐 coverage
    @[deprecated discreteUniformity_iff_setRelId_mem_uniformity (since := "2025-10-17")]
    theorem discreteUniformity_iff_idRel_mem_uniformity {X : Type u_2} [UniformSpace X] :
    DiscreteUniformity X ↔ SetRel.id ∈ uniformity X

    Alias of discreteUniformity_iff_setRelId_mem_uniformity.

    source
    📐 coverage
    theorem DiscreteUniformity.relId_mem_uniformity (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] :
    SetRel.id ∈ uniformity X
    source
    📐 coverage
    @[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
    📐 coverage
    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
    📐 coverage
    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.