dense_discrete

Mathlib.Topology.Order

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

English

In a discrete topology, a subset is dense if and only if it is the whole space.

Русский

В дискретной топологии подмножество плотно тогда, когда оно равно всему пространству.

LaTeX

$$$\\text{Dense}(S) \\iff S = \\mathrm{univ}$$$

Lean4

@[simp]
theorem dense_discrete {s : Set α} : Dense s ↔ s = univ := by simp [dense_iff_closure_eq]

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

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

Разделы

Аффилиация

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