Proposition scott_continuous_map_from_compact_basis_eq {X : dcpo} (B : compact_basis X) {Y : dcpo} (f : B → Y) (Hf : ∏ (i₁ i₂ : B), B i₁ ≪ B i₂ → f i₁ ⊑ f i₂) (i : B) : scott_continuous_map_from_basis (compact_basis_to_dcpo_basis B) f Hf (B i) = f i. Proof. use antisymm_dcpo. - apply scott_continuous_map_from_basis_le. - use less_than_dcpo_lub. + refine (i ,, _). apply is_compact_el_basis. + apply refl_dcpo. 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.