Theorems · Definition · Lie groups

IsRightUniformGroup.casesOn

{G : Type u_7} →
  [inst : UniformSpace G] →
    [inst_1 : Group G] →
      {motive : IsRightUniformGroup G → Sort u} →
        (t : IsRightUniformGroup G) →
          ([toIsTopologicalGroup : IsTopologicalGroup G] →
              (uniformity_eq : uniformity G = Filter.comap (fun x => x.2 * x.1⁻¹) (nhds 1)) → motive ⋯) →
            motive t

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceGroup