lebesgue completely dualized

[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 0a6d26112867da0461122b26ce3ce25c9cf1e411..4ba3ca3afa678e4e9878ebd20e166e582606b068 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -251,16 +251,18 @@ qed.
 
 lemma segment_ordered_set: 
   ∀O:ordered_set.∀u,v:O.ordered_set.
-intros (O u v); letin hos ≝ (half_segment_ordered_set (os_l O) u v);
-constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] 
+intros (O u v); 
+apply half2full; apply (half_segment_ordered_set (os_l O) u v); 
 qed.
 
+(*
 notation < "hvbox({[a, break b]/})" non associative with precedence 90 
   for @{'h_segment_set $a $b}.
 notation > "hvbox({[a, break b]/})" non associative with precedence 90 
   for @{'h_segment_set $a $b}.
 interpretation "Half ordered set segment" 'h_segment_set a b = 
   (half_segment_ordered_set _ a b).
+*)
 
 notation < "hvbox({[a, break b]})" non associative with precedence 90 
   for @{'segment_set $a $b}.
@@ -268,13 +270,41 @@ notation > "hvbox({[a, break b]})" non associative with precedence 90
   for @{'segment_set $a $b}.
 interpretation "Ordered set segment" 'segment_set a b = 
   (segment_ordered_set _ a b).
+  
+definition hint_sequence: 
+  ∀C:ordered_set.
+    sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
+intros;assumption;
+qed.
+
+definition hint_sequence1: 
+  ∀C:ordered_set.
+    sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C).
+intros;assumption;
+qed.
+
+definition hint_sequence2: 
+  ∀C:ordered_set.
+    sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)).
+intros;assumption;
+qed.
+
+definition hint_sequence3: 
+  ∀C:ordered_set.
+    sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)).
+intros;assumption;
+qed.
 
+coercion hint_sequence nocomposites.
+coercion hint_sequence1 nocomposites.
+coercion hint_sequence2 nocomposites.
+coercion hint_sequence3 nocomposites.
 
-(* Lemma 2.9 *)
-lemma h_segment_preserves_supremum:
-  ∀O:half_ordered_set.∀l,u:O.∀a:sequence {[l,u]/}.∀x:{[l,u]/}. 
-    increasing ? ⌊n,\fst (a n)⌋ ∧ 
-    supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
+(* Lemma 2.9 - non easily dualizable *)
+lemma segment_preserves_supremum:
+  ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
+    ⌊n,\fst (a n)⌋ is_increasing ∧ 
+    (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x.
 intros; split; cases H; clear H; 
 [1: apply H1;
 |2: cases H2; split; clear H2;
@@ -282,12 +312,17 @@ intros; split; cases H; clear H;
     |2: clear H; intro y0; apply (H3 (\fst y0));]]
 qed.
 
-notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
-notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
-
-interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
-interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
-
+lemma segment_preserves_infimum:
+  ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
+    ⌊n,\fst (a n)⌋ is_decreasing ∧ 
+    (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
+intros; split; cases H; clear H; 
+[1: apply H1;
+|2: cases H2; split; clear H2;
+    [1: apply H;
+    |2: clear H; intro y0; apply (H3 (\fst y0));]]
+qed.
+           
 (* Definition 2.10 *)
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".