completion_coe — Mathlib

English

Applying a normed group homomorphism to an element and then taking completion yields the same result as applying the homomorphism after completion.

Русский

Применение гомоморфизма к элементу и затем переход к завершению дает тот же результат, что и применение гомоморфизма после завершения.

LaTeX

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

Lean4

theorem completion_coe (f : NormedAddGroupHom G H) (g : G) : f.completion g = f g :=
  Completion.map_coe f.uniformContinuous _

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