Theorems · Theorem · Lie groups

AddMonoidHom.completion_add

∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α] {γ : Type u_5}
  [inst_3 : AddCommGroup γ] [inst_4 : UniformSpace γ] [inst_5 : IsUniformAddGroup γ] (f g : α →+ γ) (hf : Continuous ⇑f)
  (hg : Continuous ⇑g), (f + g).completion ⋯ = f.completion hf + g.completion hg

Defined in

Mathlib.Topology.Algebra.GroupCompletion

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceAddGroupIsUniformAddGroupAddCommGroupUniformSpaceIsUniformAddGroup