isLower_orderDual

Mathlib.Topology.Order.LowerUpperTopology

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

English

The dual statement: IsLower αᵒᵈ ↔ IsUpper α.

Русский

Двойственность: IsLower αᵒᵈ ↔ IsUpper α.

LaTeX

$$$IsLower(\alpha^{\mathrm{op}}) \iff IsUpper(\alpha)$$$

Lean4

theorem isLower_orderDual [Preorder α] [TopologicalSpace α] : IsLower αᵒᵈ ↔ IsUpper α :=
  isUpper_orderDual.symm

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

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

Разделы

Аффилиация

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