isUpper_orderDual

Mathlib.Topology.Order.LowerUpperTopology

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

← MathLib Explorer

English

The IsUpper property is equivalent to IsLower under order duality.

Русский

Свойство IsUpper эквивалентно IsLower после перехода к двойственному порядку.

LaTeX

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

Lean4

theorem isUpper_orderDual [Preorder α] [TopologicalSpace α] : IsUpper αᵒᵈ ↔ IsLower α :=
  by
  constructor
  · apply OrderDual.instIsLower
  · apply OrderDual.instIsUpper

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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