interpretation "constructive and" 'and x y = (And x y).
+inductive And3 (A,B,C:CProp) : CProp ≝
+ | Conj3 : A → B → C → And3 A B C.
+
+notation < "a ∧ b ∧ c" left associative with precedence 60 for @{'and3 $a $b $c}.
+
+interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
+
+inductive And4 (A,B,C:CProp) : CProp ≝
+ | Conj4 : A → B → C → And4 A B C.
+
+notation < "a ∧ b ∧ c ∧ d" left associative with precedence 60 for @{'and3 $a $b $c $d}.
+
+interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
+
inductive exT (A:Type) (P:A→CProp) : CProp ≝
ex_introT: ∀w:A. P w → exT A P.
interpretation "CProp exists" 'exists \eta.x = (exT _ x).
+inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
+ ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
+
+notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
+notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
+notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
+notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
+notation < "'fst' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi12 $x $y}.
+notation < "'snd' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi22 $x $y}.
+
+definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
+
+interpretation "exT fst" 'pi1 x = (pi1exT _ _ x).
+interpretation "exT fst 2" 'pi12 x y = (pi1exT _ _ x y).
+
+definition pi1exT23 ≝
+ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
+definition pi2exT23 ≝
+ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
+
+interpretation "exT2 fst" 'pi1 x = (pi1exT23 _ _ _ _ x).
+interpretation "exT2 snd" 'pi2 x = (pi2exT23 _ _ _ _ x).
+interpretation "exT2 fst 2" 'pi12 x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 snd 2" 'pi22 x y = (pi2exT23 _ _ _ _ x y).
+
+
definition Not : CProp → Prop ≝ λx:CProp.x → False.
interpretation "constructive not" 'not x = (Not x).
include "sandwich.ma".
include "property_exhaustivity.ma".
-lemma foo:
+lemma order_converges_bigger_lowsegment:
∀C:ordered_set.
∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
∀x:C.∀p:a order_converges x.
- ∀j.l ≤ (match p with [ex_introT xi _ ⇒ xi] j).
-intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2;
-cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5;
-cases H2; clear H2; intro; cases (H5 ? H2);
-cases (H (w2+j)); apply (H8 H6);
+ ∀j.l ≤ (fst p) j.
+intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
+intro H2; cases (H8 ? H2);
+cases (H (w1+j)); apply (H12 H7);
+qed.
+
+lemma order_converges_smaller_upsegment:
+ ∀C:ordered_set.
+ ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
+ ∀x:C.∀p:a order_converges x.
+ ∀j.(snd p) j ≤ u.
+intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
+intro H2; cases (H10 ? H2);
+cases (H (w1+j)); apply (H11 H7);
qed.
-
(* Theorem 3.10 *)
-theorem lebesgue:
+theorem lebesgue_oc:
∀C:ordered_uniform_space.
(∀l,u:C.order_continuity {[l,u]}) →
∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
(segment_ordered_uniform_space C l u))
(λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
(sig_in ?? x h).
-intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5;
-cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
+intros;
+generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
+generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
+cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
+cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
+ intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
+ apply (le_transitive ???? (H7 0)); simplify;
+ cases (H1 i); assumption;] clear H3;
+cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
+ intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
+ apply (le_transitive ????? (H7 0)); simplify;
+ cases (H1 i); assumption;] clear H2;
split;
-[2: intro h;
- cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h));
-
+[1: cases Hx; cases H3; cases Hy; cases H7; split;
+ [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
+ |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
+|2: intros 3 (h);
+ letin X ≝ (sig_in ?? x h);
+ letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
+ letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
+ letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
+ apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+ [1: intro j; cases (Hxy j); cases H3; cases H4; split;
+ [apply (H5 0);|apply (H7 0)]
+ |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
+ cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+ exists [apply w] apply H7;
+ |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+ cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+ exists [apply w] apply H7;]]
+qed.
+
(* Theorem 3.9 *)
-theorem lebesgue:
+theorem lebesgue_se:
∀C:ordered_uniform_space.property_sigma C →
(∀l,u:C.exhaustive {[l,u]}) →
∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
(segment_ordered_uniform_space C l u))
(λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
(sig_in ?? x h).
-intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8;
-cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
-lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
-lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
-cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x);
-[ split; assumption]
-split; simplify;
- [1: intro; cases (H7 n); cases H3;
-
-
- lapply (sandwich ? x xi yi a );
- [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
- |3: intros 2;
- cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x);
- [1:
-
-lapply (restrict_uniform_convergence ? H ?? (H1 l u)
- (λn:nat.sig_in ?? (a n) (H2 n)) x);
- [2:split; assumption]
\ No newline at end of file
+intros (C S);
+generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
+generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
+cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
+cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
+ intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
+ apply (le_transitive ???? (H7 0)); simplify;
+ cases (H1 i); assumption;] clear H3;
+cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
+ intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
+ apply (le_transitive ????? (H7 0)); simplify;
+ cases (H1 i); assumption;] clear H2;
+split;
+[1: cases Hx; cases H3; cases Hy; cases H7; split;
+ [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
+ |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
+|2: intros 3;
+ lapply (uparrow_upperlocated ? xi x Hx)as Ux;
+ lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
+ letin X ≝ (sig_in ?? x h);
+ letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
+ letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
+ letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
+ apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+ [1: intro j; cases (Hxy j); cases H3; cases H4; split;
+ [apply (H5 0);|apply (H7 0)]
+ |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);
+ apply (H4 h);
+ |3: cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy);
+ apply (H4 h);]]
+qed.
split; [apply H1] intros;
cases (H2 (fst y) H3); exists [apply w] assumption;
qed.
+
+lemma segment_preserves_downarrow:
+ ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h.
+ (λn.fst (a n)) ↓ x → a ↓ (sig_in ?? x h).
+intros; cases H (Ha Hx); split [apply Ha] cases Hx;
+split; [apply H1] intros;
+cases (H2 (fst y) H3); exists [apply w] assumption;
+qed.
(* Fact 2.18 *)
lemma segment_cauchy:
qed.
(* Lemma 3.8 *)
-lemma restrict_uniform_convergence:
+lemma restrict_uniform_convergence_uparrow:
∀C:ordered_uniform_space.property_sigma C →
∀l,u:C.exhaustive {[l,u]} →
∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↑ x →
[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;
- lapply (sigma_cauchy ? H ? x ? Ha); [split; assumption]
+ lapply (sigma_cauchy ? H ? x ? Ha); [left; split; assumption]
apply restric_uniform_convergence; assumption;]
qed.
-
\ No newline at end of file
+
+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 (sig_in ?? x h).
+intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
+[1: split;
+ [2: apply (infimum_is_lower_bound C ?? Hx l);
+ apply (segment_lowerbound ? l u);
+ |1: apply (le_transitive ?? (fst (a 0))); [apply H2;]
+ apply (segment_upperbound ? l u);]
+|2: intros;
+ lapply (downarrow_lowerlocated ? a (sig_in ?? x h)) as Ha1;
+ [2: apply segment_preserves_downarrow;split; assumption;]
+ lapply (segment_preserves_infimum ?l u a (sig_in ??? 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
∀U.us_unifbase ? U →
∃V:sequence (C square → Prop).
(∀i.us_unifbase ? (V i)) ∧
- ∀a:sequence C.∀x:C.a ↑ x →
+ ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) →
(∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
definition max ≝
intros; rewrite > sym_max in H; apply (max_le_l ??? H);
qed.
-
definition hide ≝ λT:Type.λx:T.x.
notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
(* Lemma 3.6 *)
lemma sigma_cauchy:
∀C:ordered_uniform_space.property_sigma C →
- ∀a:sequence C.∀l:C.a ↑ l → a is_cauchy → a uniform_converges l.
-intros 8; cases H1; cases H5; clear H5;
-cases (H ? H3); cases H5; clear H5;
+ ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
+intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
match i with
[ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
[1,2:apply H8;
|3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
simplify in ⊢ (?→? (? % ?) ?→?);
- intros; lapply (H10 i j) as H14;
- [2: apply (max_le_l ??? H11);|3:apply (max_le_l ??? H12);]
- cases (le_to_or_lt_eq ?? H13); [2: destruct H15; destruct H5; assumption]
- generalize in match H11; generalize in match H12;
+ intros; lapply (H5 i j) as H14;
+ [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
+ cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
+ generalize in match H6; generalize in match H7;
cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
- apply H16; [3: apply le_S_S_to_le; assumption]
+ apply H12; [3: apply le_S_S_to_le; assumption]
apply lt_to_le; apply (max_le_r w1); assumption;
- |4: intros; clear H11; rewrite > H5 in H10;
- rewrite < (le_n_O_to_eq ? H14); apply H10; assumption;]
+ |4: intros; clear H6; rewrite > H4 in H5;
+ rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;]
cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
intro n; change with (S (m n) ≤ m (S n)); unfold m;
whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
lapply (Hm n) as L1; change in L1 with (m n < m (S n));
lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);]
clearbody m;
-lapply (selection ?? Hm a l H1) as H10;
+cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2:
+ cases H1;
+ [ left; apply (selection_uparrow ?? Hm a l H4);
+ | right; apply (selection_downarrow ?? Hm a l H4);]]
lapply (H9 ?? H10) as H11; [
exists [apply (m 0:nat)] intros;
- apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
- simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;]
- change with (a (m O) ≤ a i);
- apply (trans_increasing ?? H4); intro; whd in H12;
- apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)]
+ cases H1;
+ [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
+ |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉);
+ lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
+ simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;]
+ [1:change with (a (m O) ≤ a i);
+ apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14);
+ |2:change with (a i ≤ a (m O));
+ apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]]
clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
generalize in match (refl_eq nat (m p));
-(*
-intro E; cases p in E : (? ? ? ?);
-*)
generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
intros (H16); simplify in H16:(? ? ? %); destruct H16;
apply H15; [3: apply le_n]
[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
- apply (le_to_not_lt p q H5);
+ apply (le_to_not_lt p q H4);
|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
- apply (le_to_not_lt p r H10);]
+ apply (le_to_not_lt p r H5);]
qed.
cases (H1 ? H) (w Hw); apply Hv; assumption;
qed.
+lemma infimum_is_lower_bound:
+ ∀C:ordered_set.∀a:sequence C.∀u:C.
+ u is_infimum a → ∀v.v is_lower_bound a → v ≤ u.
+intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
+cases (H1 ? H) (w Hw); apply Hv; assumption;
+qed.
+
+
(* Lemma 2.6 *)
definition strictly_increasing ≝
λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
for @{'strictly_decreasing $s}.
interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
(strictly_decreasing _ s).
-
-notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
-interpretation "Ordered set supremum of increasing" 'sup_inc s u =
- (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
- (increasing _ s)
- (supremum _ s u)).
-notation "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
-interpretation "Ordered set supremum of increasing" 'inf_dec s u =
- (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
- (decreasing _ s)
- (infimum _ s u)).
+
+definition uparrow ≝
+ λC:ordered_set.λs:sequence C.λu:C.
+ s is_increasing ∧ u is_supremum s.
+
+definition downarrow ≝
+ λC:ordered_set.λs:sequence C.λu:C.
+ s is_decreasing ∧ u is_infimum s.
+
+notation < "a \uparrow \nbsp u" non associative with precedence 50 for @{'sup_inc $a $u}.
+notation > "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
+interpretation "Ordered set uparrow" 'sup_inc s u = (uparrow _ s u).
+
+notation < "a \downarrow \nbsp u" non associative with precedence 50 for @{'inf_dec $a $u}.
+notation > "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
+interpretation "Ordered set downarrow" 'inf_dec s u = (downarrow _ s u).
include "nat/plus.ma".
include "nat_ordered_set.ma".
intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
qed.
+lemma trans_decreasing:
+ ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n.
+intros 5 (C a Hs n m); elim m; [
+ rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
+ intro X; cases (os_coreflexive ?? X);]
+cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
+[2: rewrite > H2; intro; cases (os_coreflexive ?? H1);
+|1: apply (le_transitive ???? (Hs ?) (H ?));
+ intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
+qed.
+
lemma trans_increasing_exc:
∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
cases (Hs n1); assumption;]
qed.
+lemma trans_decreasing_exc:
+ ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. m ≰ n → a m ≤ a n .
+intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
+intro; apply H;
+[1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *)
+ change with (n<n1); (* is sort elimination not allowed preserved by delta? *)
+ cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
+ cases (Hs n); rewrite < H3 in H2; assumption (* ogni goal di tipo Prop non è anche di tipo CProp *)
+|2: cases (os_cotransitive ??? (a n1) H2); [2:assumption]
+ cases (Hs n1); assumption;]
+qed.
+
lemma strictly_increasing_reaches:
∀C:ordered_set.∀m:sequence nat_ordered_set.
m is_strictly_increasing → ∀w.∃t.m t ≰ w.
apply (transitive_le ??? H2 Hp);]]
qed.
-lemma selection:
+lemma selection_uparrow:
∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
cases (trans_increasing_exc C ? Ia ?? H1); assumption;]
qed.
-
+
+lemma selection_downarrow:
+ ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
+ ∀a:sequence C.∀u.a ↓ u → (λx.a (m x)) ↓ u.
+intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
+[1: intro n; simplify; apply trans_decreasing_exc; [assumption] apply (Hm n);
+|2: intro n; simplify; apply Uu;
+|3: intros (y Hy); simplify; cases (Hu ? Hy);
+ cases (strictly_increasing_reaches C ? Hm w);
+ exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [assumption]
+ cases (trans_decreasing_exc C ? Ia ?? H1); assumption;]
+qed.
+
(* Definition 2.7 *)
-alias symbol "exists" = "CProp exists".
-alias symbol "and" = "constructive and".
+alias id "ExT23" = "cic:/matita/dama/cprop_connectives/exT23.ind#xpointer(1/1)".
definition order_converge ≝
λO:ordered_set.λa:sequence O.λx:O.
- ∃l:sequence O.∃u:sequence O.
- (*l is_increasing ∧ u is_decreasing ∧*) l ↑ x ∧ u ↓ x ∧
- ∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i)).
+ ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
+ (λl,u.∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i))).
notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
for @{'order_converge $a $x}.
definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
-notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
-notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
-notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
-notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
interpretation "sigma pi1" 'pi1 x = (pi1 _ _ x).
interpretation "Type exists" 'exists \eta.x =
|2: clear H; intro y0; apply (H3 (fst y0));]]
qed.
+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 *)
coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B.
definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
[1: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
|2: right; exists [apply u]; split; [apply W|apply H4]]
qed.
-
-
projects / helm.git / commitdiff