t0Space

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsUpper.t0Space

English

The upper topology on a partial order is a T0 space.

Русский

Верхняя топология на частичном порядке есть T0-пространство.

LaTeX

$$$T_0\text{-space}(\text{upper topology on } \alpha)$$$

Lean4

/-- The upper topology on a partial order is T₀. -/
instance (priority := 90) t0Space : T0Space α :=
  IsLower.t0Space (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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