continuous_extension

Mathlib.Topology.UniformSpace.Completion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.continuous_extension

English

If f: α → β is defined and β is complete, then the extension of f is continuous.

Русский

Если f: α → β определено и β полно, то продолжение f непрерывно.

LaTeX

$$$\\mathrm{Continuous}(\\mathrm{Completion.extension}(f))$$$

Lean4

@[continuity, fun_prop]
theorem continuous_extension : Continuous (Completion.extension f) :=
  cPkg.continuous_extend

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru