upperSet_le_scott

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#Topology.upperSet_le_scott

English

The upper-set topology is contained in the Scott topology: upperSet α ≤ scott α univ.

Русский

Топология верхних множеств содержится в топологии Скотта: upperSet α ≤ scott α univ.

LaTeX

$$$\\mathrm{upperSet}(\\alpha) \\le \\mathrm{scott}(\\alpha, \\mathrm{univ})$$$

Lean4

theorem upperSet_le_scott [Preorder α] : upperSet α ≤ scott α univ :=
  le_sup_left

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

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

Разделы

Аффилиация

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