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.

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

The discrete uniformity

• eq_bot : u = ⊥

theorem discreteUniformity_iff_eq_bot (X : Type u_1) [u : UniformSpace X] : DiscreteUniformity X ↔ u = ⊥

instance DiscreteUniformity.inst (X : Type u_1) : DiscreteUniformity X

The bot uniformity is the discrete uniformity.

theorem discreteUniformity_iff_eq_principal_idRel {X : Type u_2} [UniformSpace X] : DiscreteUniformity X ↔ uniformity X = Filter.principal idRel

theorem DiscreteUniformity.eq_principal_idRel (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] : uniformity X = Filter.principal idRel

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

The discrete uniformity induces the discrete topology.

theorem discreteUniformity_iff_idRel_mem_uniformity {X : Type u_2} [UniformSpace X] : DiscreteUniformity X ↔ idRel ∈ uniformity X

theorem DiscreteUniformity.idRel_mem_uniformity (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] : idRel ∈ uniformity X

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.

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.