deltaGenerated_le

Mathlib.Topology.Compactness.DeltaGeneratedSpace

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

← MathLib Explorer

English

The delta-generated topology is finer than the original topology.

Русский

Дельта-генерированная топология более тонкая (или равна) исходной топологии.

LaTeX

$$$\\deltaGenerated X \\le t_X$$$

Lean4

/-- The delta-generated topology is at least as fine as the original one. -/
theorem deltaGenerated_le : deltaGenerated X ≤ tX :=
  iSup_le_iff.mpr fun f ↦ f.2.continuous.coinduced_le

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

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

Разделы

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

Аффилиация

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