Theorems · Definition · Lie groups

IsRightUniformAddGroup.recOn

{G : Type u_7} →
  [inst : UniformSpace G] →
    [inst_1 : AddGroup G] →
      {motive : IsRightUniformAddGroup G → Sort u} →
        (t : IsRightUniformAddGroup G) →
          ([toIsTopologicalAddGroup : IsTopologicalAddGroup G] →
              (uniformity_eq : uniformity G = Filter.comap (fun x => x.2 + -x.1) (nhds 0)) → 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

UniformSpaceAddGroup