Theorems · Definition · general topology

UniformSpace.Core.casesOn

{α : Type u} →
  {motive : UniformSpace.Core α → Sort u_1} →
    (t : UniformSpace.Core α) →
      ((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) →
                motive { uniformity := uniformity, refl := refl, symm := symm, comp := comp }) →
        motive t

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

0 results in Mathlib

Foundations

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