English
If f is continuous between Scott spaces, then it is ωScottContinuous.
Русский
Если отображение между Скоттовыми пространствами непрерывно, то оно ωScott-непрерывно.
LaTeX
$$$scottContinuous\_of\_continuous(f) : \omegaScottContinuous f$.$$
Lean4
@[deprecated Topology.IsScott.ωscottContinuous_iff_continuous (since := "2025-07-02")]
theorem scottContinuous_of_continuous {α β} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β]
(f : Scott α → Scott β) (hf : _root_.Continuous f) : OmegaCompletePartialOrder.ωScottContinuous f :=
by
rw [ωScottContinuous_iff_monotone_map_ωSup]
have h : Monotone f := fun x y h ↦
by
have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet
simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩
rcases (notBelow_isOpen z).preimage hf with hf''
let hf' := hf''.monotone_map_ωSup.2
specialize hf' c
simp only [mem_preimage, notBelow, mem_setOf_eq] at hf'
rw [← not_iff_not]
simp only [ωSup_le_iff, hf', ωSup, iSup, sSup, mem_range, Chain.map_coe, Function.comp_apply, eq_iff_iff, not_forall,
OrderHom.coe_mk]
tauto
