topology_eq

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsLower.topology_eq

English

If α is equipped with the lower topology, then the topology on α is equal to the lower topology on α.

Русский

Если на α задана нижняя топология, то топология на α совпадает с нижней топологией α.

LaTeX

$$$\\mathcal{T}_{\\alpha} = \\mathrm{lowerTopology}(\\alpha)$$$

Lean4

theorem topology_eq : ‹_› = lower α :=
  topology_eq_lowerTopology

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

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

Разделы

Аффилиация

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