continuous_stoneCechUnit

Mathlib.Topology.Compactification.StoneCech

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

English

The map stoneCechUnit: α → StoneCech α is continuous.

Русский

Карта stoneCechUnit: α → StoneCech α непрерывна.

LaTeX

$$$ Continuous\left( stoneCechUnit : \alpha \to StoneCech(\alpha) \right) $$$

Lean4

theorem continuous_stoneCechUnit : Continuous (stoneCechUnit : α → StoneCech α) :=
  (T2Quotient.continuous_mk _).comp continuous_preStoneCechUnit

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

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

Разделы

Аффилиация

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