Proposition continuous_not_specialization_weq (CX : continuous_dcpo_struct X) (x y : X) : x ⊄ y ≃ (∃ (b : X), b ≪ x ∧ ¬(b ⊑ y))%logic. Proof. use weqimplimpl. - use factor_through_squash. { apply propproperty. } intros P. induction P as [ P [ HP [ p₁ p₂ ]]] ; cbn in p₂. pose (D := approximating_family CX x). assert (HD : P (⨆ D)). { unfold D. rewrite approximating_family_lub. exact p₁. } assert (H := is_scott_open_lub_inaccessible HP D HD). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ i Pi ]. refine (hinhpr (D i ,, _ ,, _)). + apply approximating_family_way_below. + intro n. apply p₂. apply (is_scott_open_upper_set HP Pi n). - use factor_through_squash. { apply propproperty. } intro b. induction b as [ b [ p₁ p₂ ]] ; cbn in p₂. apply hinhpr. refine (_ ,, upper_set_is_scott_open CX b ,, p₁ ,, _). intro p. apply p₂. apply way_below_to_le. exact p. - apply propproperty. - apply propproperty. Qed.
Require Import UniMath.MoreFoundations.All. 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.Continuous.