notBelow

Mathlib.Topology.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#notBelow

English

The set notBelow(y) = { x | x not ≤ y } is an open subset in the Scott topology.

Русский

Множество notBelow(y) = { x | x не меньше y } является открытым в Scott-топологии.

LaTeX

$$$\text{notBelow}(y) \text{ is open in } Scott(\alpha).$$$

Lean4

/-- `notBelow` is an open set in `Scott α` used
to prove the monotonicity of continuous functions -/
def notBelow (y : Scott α) :=
  {x | ¬x ≤ y}

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

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

Разделы

Аффилиация

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