dirSupInacc

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#IsLowerSet.dirSupInacc

English

If s is a lower set, then s has DirSupInacc.

Русский

Если s является нижним множеством, тогда оно имеет DirSupInacc.

LaTeX

$$$\\text{IsLowerSet}(s) \\Rightarrow \\text{DirSupInacc}(s)$$$

Lean4

theorem dirSupInacc (hs : IsLowerSet s) : DirSupInacc s :=
  hs.compl.dirSupClosed.of_compl

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

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

Разделы

Аффилиация

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