extension_coe — Mathlib

English

The extension maps agree with the original homomorphism on the embedded domain: f.extension hf (toCompl a) = f a.

Русский

Расширение согласуется с исходным гомоморфизмом на вложенной области: f.extension hf (toCompl a) = f a.

LaTeX

$$$f.extension\\; hf\\ a = f\\,a$$$

Lean4

theorem extension_coe [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) (a : α) : f.extension hf a = f a :=
  UniformSpace.Completion.extension_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

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