scottContinuousOn — Mathlib

English

Any Scott-continuous function is Scott-continuous on any set of directed sets.

Русский

Любая Scott–непрерывная функция Scott–непрерывна на любом множестве направленных множеств.

LaTeX

$$$\\mathrm{ScottContinuous}(f) \\Rightarrow \\mathrm{ScottContinuousOn}(D,f).$$$

Lean4

theorem scottContinuousOn {D : Set (Set α)} : ScottContinuous f → ScottContinuousOn D f := fun h _ _ d₂ d₃ _ hda =>
  h d₂ d₃ hda

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