English
Equivalence between Scott topology on a Scott structure and the standard Scott topology.
Русский
Эквивалентность между Scott-структурой и стандартной Scott-топологией.
LaTeX
$$$scott\_eq\_Scott: \text{Topology.scott}(\alpha) = \text{Scott.topologicalSpace}(\alpha).$$$
Lean4
@[deprecated "Use `WithScott` API" (since := "2025-07-02")]
theorem scott_eq_Scott {α} [OmegaCompletePartialOrder α] :
Topology.scott α (Set.range fun c : Chain α => Set.range c) = Scott.topologicalSpace α :=
by
ext U
letI := Topology.scott α (Set.range fun c : Chain α => Set.range c)
rw [isOpen_iff_ωScottContinuous_mem, @isOpen_iff_continuous_mem,
@Topology.IsScott.ωscottContinuous_iff_continuous _ _ (Topology.scott α (Set.range fun c : Chain α => Set.range c))
({ topology_eq_scott := rfl })]
