instIsUpper — Mathlib

English

In the dual order, if α is a preorder with a lower topology, then αᵒᵈ carries an IsUpper structure.

Русский

В двойственном порядке, если на α задана нижняя топология, то на αᵒᵈ существует структура IsUpper.

LaTeX

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

Lean4

instance _root_.OrderDual.instIsUpper [Preorder α] [TopologicalSpace α] [IsLower α] : IsUpper αᵒᵈ where
  topology_eq_upperTopology := topology_eq_lowerTopology (α := α)

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