Proposition is_strict_scott_continuous_on_bot {X Y : hSet} {DX : dcppo_struct X} {DY : dcppo_struct Y} {f : X → Y} (Hf : is_strict_scott_continuous DX DY f) : f (pointed_PartialOrder_to_point DX) = pointed_PartialOrder_to_point DY. Proof. exact (pr2 Hf). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness.