continuous_of_scottContinuous — Mathlib

English

If a function f is ωScottContinuous, then it is continuous.

Русский

Если функция f ωScott-непрерывна, то она непрерывна.

LaTeX

$$$continuous\_of\_scottContinuous(f) : Continuous f$.$$

Lean4

@[deprecated Topology.IsScott.ωscottContinuous_iff_continuous (since := "2025-07-02")]
theorem continuous_of_scottContinuous {α β} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β]
    (f : Scott α → Scott β) (hf : ωScottContinuous f) : Continuous f := by rw [continuous_def];
  exact fun s hs ↦ hs.comp hf

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