English
Under IsScott α D and a mild hypothesis hD, a function f is Scott-continuous on D iff it is continuous.
Русский
При IsScott α D и условии hD функция f являетсяScott‑непрерывной на D тогда и только тогда, когда она непрерывна.
LaTeX
$$$\\text{ScottContinuousOn}(D,f) \\iff \\text{Continuous}(f)$$$
Lean4
@[simp]
theorem scottContinuousOn_iff_continuous {D : Set (Set α)} [Topology.IsScott α D]
(hD : ∀ a b : α, a ≤ b → { a, b } ∈ D) : ScottContinuousOn D f ↔ Continuous f :=
by
refine ⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩
· rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)]
exact
⟨(isUpperSet_of_isOpen (D := univ) hu).preimage (h.monotone D hD), fun t h₀ hd₁ hd₂ a hd₃ ha ↦
image_inter_nonempty_iff.mp <|
(isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ).mp hu).2 trivial (Nonempty.image f hd₁)
(directedOn_image.mpr (hd₂.mono @(h.monotone D hD))) (h h₀ hd₁ hd₂ hd₃) ha⟩
· refine fun hf t h₀ d₁ d₂ a d₃ ↦ ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1, fun b hb ↦ ?_⟩
by_contra h
let u := (Iic b)ᶜ
have hu : IsOpen (f ⁻¹' u) := isClosed_Iic.isOpen_compl.preimage hf
rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)] at hu
obtain ⟨c, hcd, hfcb⟩ := hu.2 h₀ d₁ d₂ d₃ h
simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf] at hb
exact hfcb <| hb _ hcd
