feat(order/directed): Scott continuous functions (#18517)

We prove an insert result for directed sets when the relation is reflexive. This is then used to show that a Scott continuous function is monotone.

This result is required in the [construction of the Scott topology on a preorder](leanprover-community/mathlib4#2508) (see also #18448).

Holding PR for mathlib4: leanprover-community/mathlib4#2543



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/order/directed.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import data.set.image
 import order.lattice
 import order.max
+import order.bounds.basic
 
 /-!
 # Directed indexed families and sets
@@ -22,6 +23,11 @@ directed iff each pair of elements has a shared upper bound.
 * `directed_on r s`: Predicate stating that the set `s` is `r`-directed.
 * `is_directed α r`: Prop-valued mixin stating that `α` is `r`-directed. Follows the style of the
   unbundled relation classes such as `is_total`.
+* `scott_continuous`: Predicate stating that a function between preorders preserves
+  `is_lub` on directed sets.
+
+## References
+* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980]
 -/
 
 open function
@@ -161,6 +167,37 @@ by assumption
 instance order_dual.is_directed_le [has_le α] [is_directed α (≥)] : is_directed αᵒᵈ (≤) :=
 by assumption
 
+section reflexive
+
+lemma directed_on.insert (h : reflexive r) (a : α) {s : set α} (hd : directed_on r s)
+  (ha : ∀ b ∈ s, ∃ c ∈ s, a ≼ c ∧ b ≼ c) : directed_on r (insert a s) :=
+begin
+  rintros x (rfl | hx) y (rfl | hy),
+  { exact ⟨y, set.mem_insert _ _, h _, h _⟩ },
+  { obtain ⟨w, hws, hwr⟩ := ha y hy,
+    exact ⟨w, set.mem_insert_of_mem _ hws, hwr⟩ },
+  { obtain ⟨w, hws, hwr⟩ := ha x hx,
+    exact ⟨w, set.mem_insert_of_mem _ hws, hwr.symm⟩ },
+  { obtain ⟨w, hws, hwr⟩ := hd x hx y hy,
+    exact ⟨w, set.mem_insert_of_mem _ hws, hwr⟩ },
+end
+
+lemma directed_on_singleton (h : reflexive r) (a : α) : directed_on r ({a} : set α) :=
+λ x hx y hy, ⟨x, hx, h _, hx.symm ▸ hy.symm ▸ h _⟩
+
+lemma directed_on_pair (h : reflexive r) {a b : α} (hab : a ≼ b) :
+  directed_on r ({a, b} : set α) :=
+(directed_on_singleton h _).insert h _ $ λ c hc, ⟨c, hc, hc.symm ▸ hab, h _⟩
+
+lemma directed_on_pair' (h : reflexive r) {a b : α} (hab : a ≼ b) :
+  directed_on r ({b, a} : set α) :=
+begin
+  rw set.pair_comm,
+  apply directed_on_pair h hab,
+end
+
+end reflexive
+
 section preorder
 variables [preorder α] {a : α}
 
@@ -218,3 +255,42 @@ instance order_top.to_is_directed_le [has_le α] [order_top α] : is_directed α
 @[priority 100]  -- see Note [lower instance priority]
 instance order_bot.to_is_directed_ge [has_le α] [order_bot α] : is_directed α (≥) :=
 ⟨λ a b, ⟨⊥, bot_le, bot_le⟩⟩
+
+section scott_continuous
+
+variables [preorder α] {a : α}
+
+/--
+A function between preorders is said to be Scott continuous if it preserves `is_lub` on directed
+sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the
+Scott topology.
+
+The dual notion
+
+```lean
+∀ ⦃d : set α⦄, d.nonempty → directed_on (≥) d → ∀ ⦃a⦄, is_glb d a → is_glb (f '' d) (f a)
+```
+
+does not appear to play a significant role in the literature, so is omitted here.
+-/
+def scott_continuous [preorder β] (f : α → β) : Prop :=
+∀ ⦃d : set α⦄, d.nonempty → directed_on (≤) d → ∀ ⦃a⦄, is_lub d a → is_lub (f '' d) (f a)
+
+protected lemma scott_continuous.monotone [preorder β] {f : α → β}
+  (h : scott_continuous f) :
+  monotone f :=
+begin
+  intros a b hab,
+  have e1 : is_lub (f '' {a, b}) (f b),
+  { apply h,
+    { exact set.insert_nonempty _ _ },
+    { exact directed_on_pair le_refl hab },
+    { rw [is_lub, upper_bounds_insert, upper_bounds_singleton,
+        set.inter_eq_self_of_subset_right (set.Ici_subset_Ici.mpr hab)],
+      exact is_least_Ici } },
+  apply e1.1,
+  rw set.image_pair,
+  exact set.mem_insert _ _,
+end
+
+end scott_continuous