completion_comp — Mathlib

English

The completion of a composition equals the composition of completions: g.completion ∘ f.completion = (g ∘ f).completion.

Русский

Завершение композиции равно композиции завершений: g^{comp} ∘ f^{comp} = (g ∘ f)^{comp}.

LaTeX

$$$ g^{\mathrm{comp}} \circ f^{\mathrm{comp}} = (g \circ f)^{\mathrm{comp}}.$$$

Lean4

theorem completion_comp (f : NormedAddGroupHom G H) (g : NormedAddGroupHom H K) :
    g.completion.comp f.completion = (g.comp f).completion :=
  by
  ext x
  rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def, NormedAddGroupHom.completion_coe_to_fun,
    NormedAddGroupHom.completion_coe_to_fun, Completion.map_comp g.uniformContinuous f.uniformContinuous]
  rfl

Похожие утверждения