instDiscreteTopology

Mathlib.Topology.UniformSpace.DiscreteUniformity

URI: https://scilib.ai/kg/mathlib#DiscreteUniformity.instDiscreteTopology

← MathLib Explorer

English

The discrete uniformity induces the discrete topology on X.

Русский

Дискретная равномерность порождает дискретную топологию на X.

LaTeX

$$$\text{DiscreteTopology } X$$$

Lean4

/-- The discrete uniformity induces the discrete topology. -/
instance : DiscreteTopology X where
  eq_bot := by rw [DiscreteUniformity.eq_bot (X := X), UniformSpace.toTopologicalSpace_bot]

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

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

Разделы

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

Аффилиация

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