instTopologicalSpace

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLower.instTopologicalSpace

English

WithLower α carries the lower topology, i.e., its topology is the generated one from the lower sets.

Русский

WithLower α имеет нижнюю топологию, т. е. ее топология — генерация по нижним множествам.

LaTeX

$$TopologicalSpace(WithLower α) := lower (WithLower α)$$

Lean4

instance : TopologicalSpace (WithLower α) :=
  lower (WithLower α)

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

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

Разделы

Аффилиация

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