Theorems · Theorem · general topology

UniformSpace.Core.mk.inj

∀ {α : Type u} {uniformity : Filter (α × α)} {refl : Filter.principal SetRel.id ≤ uniformity}
  {symm : Filter.Tendsto Prod.swap uniformity uniformity}
  {comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity} {uniformity_1 : Filter (α × α)}
  {refl_1 : Filter.principal SetRel.id ≤ uniformity_1} {symm_1 : Filter.Tendsto Prod.swap uniformity_1 uniformity_1}
  {comp_1 : (uniformity_1.lift' fun s => SetRel.comp s s) ≤ uniformity_1},
  { uniformity := uniformity, refl := refl, symm := symm, comp := comp } =
      { uniformity := uniformity_1, refl := refl_1, symm := symm_1, comp := comp_1 } →
    uniformity = uniformity_1

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

1 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound