Scott-continuous maps (Scott 1972, §2.5–2.7)

def Domain.ContinuousLattice.PreservesDirectedSup {D : Type u_1} {D' : Type u_2} [CompleteLattice D] [CompleteLattice D'] (f : D → D') : Prop

A function preserves suprema of nonempty directed subsets.

Equations

• Domain.ContinuousLattice.PreservesDirectedSup f = ∀ ⦃S : Set D⦄, S.Nonempty → DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) S → f (sSup S) = sSup (f '' S)

theorem Domain.ContinuousLattice.preservesDirectedSup_monotone {D : Type u_1} {D' : Type u_2} [CompleteLattice D] [CompleteLattice D'] {f : D → D'} (hf : PreservesDirectedSup f) : Monotone f

theorem Domain.ContinuousLattice.scottOpen_preimage {D : Type u_1} {D' : Type u_2} [CompleteLattice D] [CompleteLattice D'] {f : D → D'} (hf : PreservesDirectedSup f) {U : Set D'} (hU : ScottOpen U) : ScottOpen (f ⁻¹' U)

theorem Domain.ContinuousLattice.continuous_of_preservesDirectedSup {D : Type u_1} {D' : Type u_2} [CompleteLattice D] [CompleteLattice D'] {f : D → D'} (hf : PreservesDirectedSup f) : Continuous f

theorem Domain.ContinuousLattice.continuous_preservesDirectedSup {D : Type u_1} {D' : Type u_2} [CompleteLattice D] [CompleteLattice D'] {f : D → D'} (hf : Continuous f) : PreservesDirectedSup f

theorem Domain.ContinuousLattice.proposition_2_5 {D : Type u_1} {D' : Type u_2} [CompleteLattice D] [CompleteLattice D'] (f : D → D') : Continuous f ↔ PreservesDirectedSup f

Scott 1972, Proposition 2.5. Scott continuity ↔ preservation of directed suprema.

Proposition 2.6

theorem Domain.ContinuousLattice.proposition_2_6 {D : Type u_1} {D' : Type u_2} {D'' : Type u_3} [CompleteLattice D] [CompleteLattice D'] [CompleteLattice D''] (f : D × D' → D'') : PreservesDirectedSup f ↔ (∀ (y : D'), PreservesDirectedSup fun (x : D) => f (x, y)) ∧ ∀ (x : D), PreservesDirectedSup fun (y : D') => f (x, y)

Scott 1972, Proposition 2.6. A function of several variables between complete lattices is (Scott-)continuous jointly iff it is continuous in each variable separately. Continuity is phrased as preservation of directed suprema (Proposition 2.5); it suffices to treat two variables, the product D × D' carrying the componentwise complete-lattice structure (whose induced topology is the product topology).

Proposition 2.7

theorem Domain.ContinuousLattice.proposition_2_7_sup {D : Type u_1} [CompleteLattice D] : Continuous fun (p : D × D) => p.1 ⊔ p.2

Scott 1972, Proposition 2.7 (join). Binary join is Scott-continuous on every complete lattice; this is the ⊔-part of Scott's 2.7.

theorem Domain.ContinuousLattice.meet_preservesDirectedSup {D : Type u_1} [CompleteLattice D] (x : D) (hD : IsContinuousLattice D) : PreservesDirectedSup fun (z : D) => x ⊓ z

theorem Domain.ContinuousLattice.proposition_2_7_inf_left {D : Type u_1} [CompleteLattice D] (hD : IsContinuousLattice D) (y : D) : Continuous fun (x : D) => x ⊓ y

Scott 1972, Proposition 2.7 (meet, separate). On a continuous lattice, x ↦ x ⊓ y and y ↦ x ⊓ y are Scott-continuous; Scott's full 2.7 also covers joint continuity on the product via Proposition 2.6.

theorem Domain.ContinuousLattice.proposition_2_7_inf_right {D : Type u_1} [CompleteLattice D] (hD : IsContinuousLattice D) (x : D) : Continuous fun (y : D) => x ⊓ y