dense_univ

Mathlib.Topology.Closure

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

English

In any topological space X, the entire space is dense in X.

Русский

В любом топологическом пространстве X множество всего пространства плотно в X.

LaTeX

$$$\overline{\mathrm{univ}} = \mathrm{univ}$$$

Lean4

@[simp]
theorem dense_univ : Dense (univ : Set X) := fun _ => subset_closure trivial

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

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

Разделы

Аффилиация

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