continuous_preStoneCechExtend

Mathlib.Topology.Compactification.StoneCech

URI: https://scilib.ai/kg/mathlib#continuous_preStoneCechExtend

English

The extension preStoneCechExtend hg is continuous.

Русский

Расширение preStoneCechExtend hg непрерывно.

LaTeX

$$$ Continuous( preStoneCechExtend hg ) $$$

Lean4

theorem continuous_preStoneCechExtend : Continuous (preStoneCechExtend hg) :=
  continuous_quot_lift _ (continuous_ultrafilter_extend g)

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

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

Разделы

Аффилиация

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