qed.
record ordered_set : Type ≝ {
- os_l : half_ordered_set;
+ os_l_ : half_ordered_set;
os_r_ : half_ordered_set;
- os_with : os_r_ = dual_hos os_l
+ os_with : os_r_ = dual_hos os_l_
}.
+definition os_l : ordered_set → half_ordered_set.
+intro h; constructor 1;
+[ apply (hos_carr (os_l_ h));
+| apply (λx,y.hos_excess (os_l_ h) x y);
+| apply (hos_coreflexive (os_l_ h));
+| apply (hos_cotransitive (os_l_ h));
+]
+qed.
+
definition os_r : ordered_set → half_ordered_set.
-intro o; apply (dual_hos (os_l o)); qed.
+intro o; apply (dual_hos (os_l_ o)); qed.
+
+lemma half2full : half_ordered_set → ordered_set.
+intro hos;
+constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity]
+qed.
+
+(* coercion half2full. *)
definition Type_of_ordered_set : ordered_set → Type.
intro o; apply (hos_carr (os_l o)); qed.
apply (restrict ? l u ??? H4); apply (Hm ? H1);
qed.
-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.
-
definition order_continuity ≝
λC:ordered_uniform_space.∀a:sequence C.∀x:C.
(a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).
|2: intros;
lapply (uparrow_upperlocated a ≪x,h≫) as Ha1;
[2: apply (segment_preserves_uparrow C l u);split; assumption;]
- lapply (segment_preserves_supremum l u a ≪?,h≫) as Ha2;
+ lapply (segment_preserves_supremum C l u a ≪?,h≫) as Ha2;
[2:split; assumption]; cases Ha2; clear Ha2;
cases (H1 a a); lapply (H6 H4 Ha1) as HaC;
lapply (segment_cauchy ? l u ? HaC) as Ha;
coercion hint_mah4 nocomposites.
-axiom restrict_uniform_convergence_downarrow:
+lemma restrict_uniform_convergence_downarrow:
∀C:ordered_uniform_space.property_sigma C →
∀l,u:C.exhaustive {[l,u]} →
∀a:sequence {[l,u]}.∀x: C. ⌊n,\fst (a n)⌋ ↓ x →
x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫.
- (*
intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
[1: split;
[2: apply (infimum_is_lower_bound ? x Hx l);
apply (segment_upperbound ? l u a 0);]
|2: intros;
lapply (downarrow_lowerlocated a ≪x,h≫) as Ha1;
- [2: apply (segment_preserves_downarrow ? l u);split; assumption;]
- lapply (segment_preserves_infimum l u);
- [2: apply a; ≪?,h≫) as Ha2;
+ [2: apply (segment_preserves_downarrow ? l u);split; assumption;]
+ lapply (segment_preserves_infimum C l u a ≪x,h≫) as Ha2;
[2:split; assumption]; cases Ha2; clear Ha2;
cases (H1 a a); lapply (H7 H4 Ha1) as HaC;
lapply (segment_cauchy ? l u ? HaC) as Ha;
lapply (sigma_cauchy ? H ? x ? Ha); [right; split; assumption]
apply restric_uniform_convergence; assumption;]
qed.
-*)
\ No newline at end of file
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}.
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;
|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".
projects / helm.git / commitdiff