English
ScottContinuousOn D f means f preserves IsLUB on directed sets from D.
Русский
ScottContinuousOn D f означает, что f сохраняет на directed множества IsLUB из D.
LaTeX
$$$\\mathrm{ScottContinuousOn}(D,f) \\iff \\forall d \\in D, d \\neq \\varnothing \\rightarrow \\mathrm{DirectedOn}(\\le, d) \\rightarrow \\forall a, \\mathrm{IsLUB}\\ d\\ a \\rightarrow \\mathrm{IsLUB}(f''d)(f a).$$$
Lean4
/-- A function between preorders is said to be Scott continuous on a set `D` of directed sets if it
preserves `IsLUB` on elements of `D`.
The dual notion
```lean
∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≥ ·) d → ∀ ⦃a⦄, IsGLB d a → IsGLB (f '' d) (f a)
```
does not appear to play a significant role in the literature, so is omitted here.
-/
def ScottContinuousOn (D : Set (Set α)) (f : α → β) : Prop :=
∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → IsLUB (f '' d) (f a)
