topology_eq

Mathlib.Topology.Order.ScottTopology

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

English

If IsScott α D holds, then the current Scott topology coincides with scott α D, i.e. topology_eq.

Русский

Если выполняется IsScott α D, то текущая топология совпадает с топологией Скотта: topology_eq.

LaTeX

$$$[\\text{IsScott } \\alpha D] \\Rightarrow \\mathrm{topology\\_eq} = \\mathrm{scott}(\\alpha, D)$$$

Lean4

theorem topology_eq [IsScott α D] : ‹_› = scott α D :=
  topology_eq_scott

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

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

Разделы

Аффилиация

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