Proposition approximating_compact_basis_lub (B : compact_basis) (x : X) : ⨆ (directed_set_from_compact_basis B x) = x. Proof. use antisymm_dcpo. - use dcpo_lub_is_least. intro i. exact (pr2 i). - use (is_least_upperbound_is_least (is_least_upperbound_compact_basis B x)). apply is_least_upperbound_is_upperbound. exact (is_least_upperbound_dcpo_lub (directed_set_from_compact_basis B x)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis.