instClosedIicTopologyOrderDual — Mathlib

English

The dual (opposite) order of α inherits a ClosedIciTopology from α; equivalently, the dual order has a closed analogue for the dual notions.

Русский

Обратный порядок α наследует ClosedIciTopology; эквивалентно, в двойственном порядке сохраняются соответствующие замкнутые свойства.

LaTeX

$$$ ClosedIicTopology (OrderDual\, α) $$$

Lean4

instance : ClosedIicTopology αᵒᵈ where isClosed_Iic _ := isClosed_Ici (α := α)

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