proposition: Proposition strongly_maximal_pair {a : A} {b : B} (Ha : is_strongly_maximal a) (Hb : is_strongly_maximal b) : @is_strongly_maximal (A × B)%dcpo (a ,, b).
proof: Proof. intros ( x₁ & y₁ ) ( x₂ & y₂ ) q. pose (p₁ := way_below_prod_pr1 basis_B q : x₁ ≪ x₂). pose (p₂ := way_below_prod_pr2 basis_A q : y₁ ≪ y₂). assert (H := Ha x₁ x₂ p₁). revert H. use factor_through_squash_hProp. intros H₁. assert (H := Hb y₁ y₂ p₂). revert H. use factor_through_squash_hProp. intros H₂. induction H₁ as [ H₁ | H₁ ], H₂ as [ H₂ | H₂ ]. - use hdisj_in1. use to_way_below_prod. + exact H₁. + exact H₂. - use hdisj_in2. revert H₂. use factor_through_squash_hProp. intros ( P₁ & P₂ & r₁ & r₂ & r₃ ). refine (hinhpr _). refine (prod_scott_open (true_scott_open_set _) P₁ ,, _). refine (prod_scott_open (true_scott_open_set _) P₂ ,, _ ,, _ ,, _) ; cbn. + exact (tt ,, r₁). + exact (tt ,, r₂). + intros ( x₃ & y₃ ). intros ( ( _ & s₁ ) & ( _ & s₂ ) ) ; cbn in s₁, s₂. exact (r₃ _ (s₁ ,, s₂)). - use hdisj_in2. revert H₁. use factor_through_squash_hProp. intros ( P₁ & P₂ & r₁ & r₂ & r₃ ). refine (hinhpr _). refine (prod_scott_open P₁ (true_scott_open_set _) ,, _). refine (prod_scott_open P₂ (true_scott_open_set _) ,, _ ,, _ ,, _) ; cbn. + exact (r₁ ,, tt). + exact (r₂ ,, tt). + intros ( x₃ & y₃ ). intros ( ( s₁ & _ ) & ( s₂ & _ ) ) ; cbn in s₁, s₂. exact (r₃ _ (s₁ ,, s₂)). - use hdisj_in2. revert H₁. use factor_through_squash_hProp. intros ( P₁ & P₂ & r₁ & r₂ & r₃ ). refine (hinhpr _). refine (prod_scott_open P₁ (true_scott_open_set _) ,, _). refine (prod_scott_open P₂ (true_scott_open_set _) ,, _ ,, _ ,, _) ; cbn. + exact (r₁ ,, tt). + exact (r₂ ,, tt). + intros ( x₃ & y₃ ). intros ( ( s₁ & _ ) & ( s₂ & _ ) ) ; cbn in s₁, s₂. exact (r₃ _ (s₁ ,, s₂)). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal