scott_eq_upper_of_completeLinearOrder

English

On a complete linear order, the Scott topology equals the upper topology.

Русский

На полном линейном порядке топология Скотта совпадает с верхней топологией.

LaTeX

$$$\\mathrm{scott}(\\alpha,\\mathrm{univ}) = \\mathrm{upper}(\\alpha)$$$

Lean4

theorem scott_eq_upper_of_completeLinearOrder : scott α univ = upper α :=
  by
  letI := upper α
  ext U
  rw [@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α) ({ topology_eq_upperTopology := rfl }) U]
  letI := scott α univ
  rw [@isOpen_iff_Iic_compl_or_univ _ _ (scott α univ) ({ topology_eq_scott := rfl }) U]
    /- The upper topology on a complete linear order is the Scott topology -/

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