Scott continuity on complete lattices

Main results

• scottContinuous_iff_map_sSup: A function is Scott continuous if and only if it commutes with sSup on directed sets.

theorem scottContinuous_iff_map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {f : α → β} : ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → f (sSup d) = sSup (f '' d)

theorem ScottContinuous.map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {f : α → β} : ScottContinuous f → ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → f (sSup d) = sSup (f '' d)

Alias of the forward direction of scottContinuous_iff_map_sSup.

theorem ScottContinuous.of_map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {f : α → β} : (∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → f (sSup d) = sSup (f '' d)) → ScottContinuous f

Alias of the reverse direction of scottContinuous_iff_map_sSup.

In a complete linear order, the Scott Topology coincides with the Upper topology, see Topology.IsScott.scott_eq_upper_of_completeLinearOrder

theorem scottContinuous_inf_right {β : Type u_2} [CompleteLinearOrder β] (a : β) : ScottContinuous fun (b : β) => min a b

theorem scottContinuous_inf_left {β : Type u_2} [CompleteLinearOrder β] (b : β) : ScottContinuous fun (a : β) => min a b

theorem ScottContinuous.inf₂ {β : Type u_2} [CompleteLinearOrder β] : ScottContinuous fun (x : β × β) => match x with | (a, b) => min a b