orderDual — Mathlib

English

Density is preserved when passing to the order dual: if s is dense in α, then s viewed in αᵒᵈ is dense there as well.

Русский

Плотность сохраняется при переходе к двойственному порядку: если s плотно в α, то j рассматриванный как подмножество αᵒᵈ также плотно.

LaTeX

$$$\text{Dense } s\Rightarrow Dense\ (OrderDual.ofDual^{-1}'\ s).$$$

Lean4

theorem orderDual [TopologicalSpace α] {s : Set α} (hs : Dense s) : Dense (OrderDual.ofDual ⁻¹' s) :=
  hs

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