Theorems · Definition · Lie groups

AddMonoidHom.extension

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

Extension to the completion of a continuous group hom.

Defined in

Mathlib.Topology.Algebra.GroupCompletion

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpaceAddGroupIsUniformAddGroupUniformSpaceAddGroupIsUniformAddGroupCompleteSpaceT0Space