seg_u/l were inverted, more work

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 7bb684fd897ea243cded37e668e7ba9cfa026cc7..8ee17fc7d557d8899e04814af805174930ef3055 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -209,10 +209,10 @@ notation "𝕝 \sub term 90 s p" non associative with precedence 45 for @{'low $
  
 definition seg_u ≝
  λO:half_ordered_set.λs:segment O.λP: O → CProp.
-   wloss O ? (λl,u.P u) (seg_l_ ? s) (seg_u_ ? s).
+   wloss O ? (λl,u.P u) (seg_u_ ? s) (seg_l_ ? s).
 definition seg_l ≝
  λO:half_ordered_set.λs:segment O.λP: O → CProp.
-   wloss O ? (λl,u.P u) (seg_u_ ? s) (seg_l_ ? s). 
+   wloss O ? (λl,u.P u) (seg_l_ ? s) (seg_u_ ? s). 
  
 interpretation "uppper" 'upp s P = (seg_u (os_l _) s P).
 interpretation "lower" 'low s P = (seg_l (os_l _) s P).
@@ -221,7 +221,7 @@ interpretation "lower dual" 'low s P = (seg_u (os_r _) s P).
  
 definition in_segment ≝ 
   λO:half_ordered_set.λs:segment O.λx:O.
-    wloss O ? (λp1,p2.p1 ∧ p2) (seg_u ? s (λu.u ≤≤ x)) (seg_l ? s (λl.x ≤≤ l)).
+    wloss O ? (λp1,p2.p1 ∧ p2) (seg_l ? s (λl.l ≤≤ x)) (seg_u ? s (λu.x ≤≤ u)).
 
 notation "‡O" non associative with precedence 90 for @{'segment $O}.
 interpretation "Ordered set sergment" 'segment x = (segment x).
@@ -360,12 +360,14 @@ qed.
 *)
        
 (* Definition 2.10 *)
+
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
+(*
 definition square_segment ≝ 
   λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
     in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
- 
+*) 
 definition convex ≝
   λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
     ∀s.U s → le O (\fst s) (\snd s) →