English
For predicate-valued maps, Scott-continuity is equivalent to ordinary continuity under the Scott topology, i.e., a function f: α → Prop is ωScottContinuous iff it is continuous.
Русский
Для отображений в булевы значенияScott-непрерывность эквивалентна обычной непрерывности под Scott-топологией; функция f: α → Prop непрерывна тогда и только тогда, когда она ωScott-непрерывна.
LaTeX
$$$\omegaScottContinuous f \;\iff\; \text{Continuous } f,$
при заданной структуре IsScott на α.$$
Lean4
@[simp]
theorem ωScottContinuous_iff_continuous {α : Type*} [OmegaCompletePartialOrder α] [TopologicalSpace α]
[Topology.IsScott α (Set.range fun c : Chain α => Set.range c)] {f : α → Prop} :
ωScottContinuous f ↔ Continuous f := by
rw [ωScottContinuous,
scottContinuousOn_iff_continuous
(fun a b hab => by use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab)]
