Proposition is_least_upperbounded_union_open {I : UU} (P : I → scott_open_set D) (Q : scott_open_set D) (HQ : is_upperbound_lattice bounded_lattice_scott_open_set P Q) : Lle bounded_lattice_scott_open_set (scott_open_set_union P) Q. Proof. use bounded_lattice_scott_open_set_le. intros x. use factor_through_squash_hProp. intros i. induction i as [ i Hi ]. exact (from_bounded_lattice_scott_open_set_le (HQ i) Hi). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Examples.IdealCompletion. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting.