Theorems · Definition · general topology

UniformSpace.casesOn

{α : Type u} →
  {motive : UniformSpace α → Sort u_1} →
    (t : UniformSpace α) →
      ([toTopologicalSpace : TopologicalSpace α] →
          (uniformity : Filter (α × α)) →
            (symm : Filter.Tendsto Prod.swap uniformity uniformity) →
              (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity) →
                (nhds_eq_comap_uniformity : ∀ (x : α), nhds x = Filter.comap (Prod.mk x) uniformity) →
                  motive
                    { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
                      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity }) →
        motive t

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound