English
The completion of the sum of two additive homomorphisms equals the sum of their completions (alternative form).
Русский
Дополнение суммы двух аддитивных гомоморфизмов равно сумме их дополнений (альтернативная формулировка).
LaTeX
$$$ (f+g).completion hf hg = f.completion hf + g.completion hg $$$
Lean4
theorem completion_add {γ : Type*} [AddCommGroup γ] [UniformSpace γ] [IsUniformAddGroup γ] (f g : α →+ γ)
(hf : Continuous f) (hg : Continuous g) :
AddMonoidHom.completion (f + g) (hf.add hg) = AddMonoidHom.completion f hf + AddMonoidHom.completion g hg :=
by
have hfg := hf.add hg
ext x
refine Completion.induction_on x ?_ ?_
·
exact
isClosed_eq ((f + g).continuous_completion hfg) ((f.continuous_completion hf).add (g.continuous_completion hg))
· simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]
