Theorems · Definition · Lie groups

AddMonoidHom.completion

{α : Type u_3} →
  {β : Type u_4} →
    [inst : UniformSpace α] →
      [inst_1 : AddGroup α] →
        [inst_2 : IsUniformAddGroup α] →
          [inst_3 : UniformSpace β] →
            [inst_4 : AddGroup β] →
              [inst_5 : IsUniformAddGroup β] →
                (f : α →+ β) → Continuous ⇑f → UniformSpace.Completion α →+ UniformSpace.Completion β

Completion of a continuous group hom, as a group hom.

Defined in

Mathlib.Topology.Algebra.GroupCompletion

Cited by

7 results in Mathlib

Foundations

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

Assumes

UniformSpaceAddGroupIsUniformAddGroupUniformSpaceAddGroupIsUniformAddGroup