denseRange_preStoneCechUnit

Mathlib.Topology.Compactification.StoneCech

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

← MathLib Explorer

English

The map preStoneCechUnit: α → PreStoneCech α has dense range.

Русский

Отображение preStoneCechUnit: α → PreStoneCech α имеет плотное образующее.

LaTeX

$$$DenseRange\left(preStoneCechUnit : α \to PreStoneCech α\right)$$$

Lean4

theorem denseRange_preStoneCechUnit : DenseRange (preStoneCechUnit : α → PreStoneCech α) :=
  Quot.mk_surjective.denseRange.comp denseRange_pure continuous_coinduced_rng

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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