proposition: Proposition is_scott_continuous_map_from_basis : is_scott_continuous (pr2 X) (pr2 Y) map_from_basis.
proof: Proof. use make_is_scott_continuous. - exact map_from_basis_monotone. - exact map_from_basis_lub. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous