dirSupClosed

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#IsUpperSet.dirSupClosed

English

If s is an upper set, then s is DirSupClosed.

Русский

Если s является верхним множеством, то оно DirSupClosed.

LaTeX

$$$\\text{IsUpperSet}(s) \\Rightarrow \\text{DirSupClosed}(s)$$$

Lean4

theorem dirSupClosed (hs : IsUpperSet s) : DirSupClosed s := fun _d ⟨_b, hb⟩ _ _a ha hds ↦ hs (ha.1 hb) <| hds hb

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

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

Разделы

Аффилиация

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