instUnivSetOfIsUpper — Mathlib

English

Let α be a complete linear order equipped with a topology that makes all upper sets open. Then the Scott topology on α coincides with this upper topology.

Русский

Пусть α — это полная линейная упорядоченная система, снабженная топологией, в которой открыты все верхние множества. Тогда скоттовская топология на α совпадает с этой верхней топологией.

LaTeX

$$$\mathrm{ScottTop}_{univ}(\alpha) = \mathrm{UpperTop}(\alpha).$$$

Lean4

instance [TopologicalSpace α] [IsUpper α] : IsScott α univ where
  topology_eq_scott := by
    rw [scott_eq_upper_of_completeLinearOrder]
    exact IsUpper.topology_eq α

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