forall_open_iff_discrete

Mathlib.Topology.Order

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

← MathLib Explorer

English

(∀ s, IsOpen s) ↔ DiscreteTopology X

Русский

(∀ s, IsOpen s) ↔ Дискретная топология X

LaTeX

$$$(\forall S: Set X, IsOpen(S)) \iff DiscreteTopology(X)$$$

Lean4

@[deprecated discreteTopology_iff_forall_isOpen (since := "2025-10-10")]
theorem forall_open_iff_discrete {X : Type*} [TopologicalSpace X] : (∀ s : Set X, IsOpen s) ↔ DiscreteTopology X :=
  discreteTopology_iff_forall_isOpen.symm

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

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

Разделы

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

Аффилиация

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