Theorems · Definition · Lie groups

IsLeftUniformGroup.recOn

{G : Type u_7} →
  [inst : UniformSpace G] →
    [inst_1 : Group G] →
      {motive : IsLeftUniformGroup G → Sort u} →
        (t : IsLeftUniformGroup G) →
          ([toIsTopologicalGroup : IsTopologicalGroup G] →
              (uniformity_eq : uniformity G = Filter.comap (fun x => x.1⁻¹ * x.2) (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