proposition: 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: 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.
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 UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis