intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SSa ? H2) (w Hw); simplify in Hw;
+intro H2; cases (SSa l H2) (w Hw); simplify in Hw;
cases (H (w+j)) (Hal Hau); apply (Hau Hw);
qed.
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;
+ apply (ge_transitive u ??? (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;
+ apply (le_transitive l ? (yi i) ? (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]
+ [1: apply (ge_transitive u ?? ? (H8 0)); cases (Hyi 0); assumption
+ |2: apply (le_transitive l ? x ? (H4 0)); cases (Hxi 0); assumption]
|2: intros 3 (h);
letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
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;
+ apply (ge_transitive u ?? ? (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;
+ apply (le_transitive l ? (yi i) ? (H7 0)); simplify;
cases (H1 i); assumption;] clear H2;
letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy);
split; [1: assumption]
intros 3;
-lapply (uparrow_upperlocated ? xi x Hx)as Ux;
-lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
+lapply (uparrow_upperlocated xi x Hx)as Ux;
+lapply (downarrow_lowerlocated yi x Hy)as Uy;
letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
intro j; cases (Hxy j); cases H7; cases H8; split; [apply (H9 0);|apply (H11 0)]
nth_height f j = q → nth_base f j < i → j < \len f →
(∀n.n<j → nth_base f n < i) →
(∀n.j < n → n < \len f → i ≤ nth_base f n) → value_spec f i q.
+
+definition match_pred ≝
+ λi.λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false].
+
+definition match_domain ≝
+ λf: list bar.λi:ratio. pred (find ? (match_pred i) f ▭).
+
+definition value_simple ≝
+ λf: list bar.λi:ratio. nth_height f (match_domain f i).
alias symbol "lt" (instance 5) = "Q less than".
alias symbol "lt" (instance 6) = "natural 'less than'".
∀f:list bar.sorted q2_lt f → O < length bar f →
∀i:ratio.nth_base f O < Qpos i → ∃p:ℚ×ℚ.value_spec f (Qpos i) p.
intros (f bars_sorted_f len_bases_gt_O_f i bars_begin_OQ_f);
-letin P ≝
- (λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false]);
-exists [apply (nth_height f (pred (find ? P f ▭)));]
-apply (value_of ?? (pred (find ? P f ▭)));
+exists [apply (value_simple f i);]
+apply (value_of ?? (match_domain f i));
[1: reflexivity
-|2: cases (cases_find bar P f ▭);
+|2: unfold match_domain; cases (cases_find bar (match_pred i) f ▭);
[1: cases i1 in H H1 H2 H3; simplify; intros;
[1: generalize in match (bars_begin_OQ_f);
cases (len_gt_non_empty ?? (len_bases_gt_O_f)); simplify; intros;
assumption;
|2: cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H3;
- intros; lapply (H3 n (le_n ?)) as K; unfold P in K;
+ intros; lapply (H3 n (le_n ?)) as K; unfold match_pred in K;
cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ n))) in K;
simplify; intros; [destruct H5] assumption]
|2: destruct H; cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H2;
simplify; intros; lapply (H (\len l) (le_n ?)) as K; clear H;
- unfold P in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
+ unfold match_pred in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
simplify; intros; [destruct H2] assumption;]
-|5: intro; cases (cases_find bar P f ▭); intros;
+|5: intro; unfold match_domain; cases (cases_find bar (match_pred i) f ▭); intros;
[1: generalize in match (bars_sorted_f);
cases (list_break ??? H) in H1; rewrite > H6;
- rewrite < H1; simplify; rewrite > nth_len; unfold P;
+ rewrite < H1; simplify; rewrite > nth_len; unfold match_pred;
cases (q_cmp (Qpos i) (\fst x)); simplify;
intros (X Hs); [2: destruct X] clear X;
cases (sorted_pivot q2_lt ??? ▭ Hs);
repeat rewrite < plus_n_Sm; rewrite < plus_n_O; simplify;
rewrite > sym_plus; rewrite < minus_plus_m_m; reflexivity;]
rewrite > len_append; rewrite > H1; simplify; rewrite < plus_n_SO;
- apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H P;
+ apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H;
elim (\len f) in i1 n H5; [cases (not_le_Sn_O ? H);]
simplify; cases n2; [ repeat rewrite < minus_n_O; apply le_S_S_to_le; assumption]
cases n1 in H1; [intros; rewrite > eq_minus_n_m_O; apply le_O_n]
|2: cases (not_le_Sn_n i1); rewrite > H in ⊢ (??%);
apply (trans_le ??? ? H4); cases i1 in H3; intros; apply le_S_S;
[ apply le_O_n; | assumption]]
-|3: cases (cases_find bar P f ▭); [
+|3: unfold match_domain; cases (cases_find bar (match_pred i) f ▭); [
cases i1 in H; intros; simplify; [assumption]
apply lt_S_to_lt; assumption;]
rewrite > H; cases (\len f) in len_bases_gt_O_f; intros; [cases (not_le_Sn_O ? H3)]
simplify; apply le_n;
-|4: intros; cases (cases_find bar P f ▭) in H; simplify; intros;
+|4: intros; unfold match_domain in H; cases (cases_find bar (match_pred i) f ▭) in H; simplify; intros;
[1: lapply (H3 n); [2: cases i1 in H4; intros [assumption] apply le_S; assumption;]
- unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
+ unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
simplify; intros; [destruct H6] assumption;
|2: destruct H; cases f in len_bases_gt_O_f H2 H3; clear H1; simplify; intros;
[cases (not_le_Sn_O ? H)] lapply (H1 n); [2: apply le_S; assumption]
- unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
+ unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
simplify; intros; [destruct H4] assumption;]]
qed.
| apply bars_begin_lt_Qpos;]
qed.
-alias symbol "lt" (instance 5) = "natural 'less than'".
-alias symbol "lt" (instance 4) = "Q less than".
-lemma value_simpl:
- ∀f:list bar.sorted q2_lt f → O < (length bar f) →
- ∀i:ratio.nth_base f O < Qpos i → ℚ × ℚ.
-intros; cases (value_lemma f H H1 i H2); assumption;
-qed.
-
lemma cases_value : ∀f,i. value_spec (bars f) (Qpos i) (value f i).
intros; unfold value;
cases (value_lemma (bars f) (bars_sorted f) (len_bases_gt_O f) i (bars_begin_lt_Qpos f i));
assumption;
qed.
-lemma cases_value_simpl :
- ∀f,H1,H2,i,Hi.value_spec f (Qpos i) (value_simpl f H1 H2 i Hi).
-intros; unfold value_simpl; cases (value_lemma f H1 H2 i Hi);
-assumption;
-qed.
-
definition same_values ≝ λl1,l2:q_f.∀input. value l1 input = value l2 input.
-definition same_values_simpl ≝
- λl1,l2:list bar.∀H1,H2,H3,H4,input,Hi1,Hi2.
- value_simpl l1 H1 H2 input Hi1 = value_simpl l2 H3 H4 input Hi2.
-
-lemma value_head :
- ∀x,y,l,H1,H2,i,H3.
- Qpos i ≤ \fst x → value_simpl (y::x::l) H1 H2 i H3 = \snd y.
-intros; cases (cases_value_simpl ? H1 H2 i H3);
-cases j in H4 H5 H6 H7 H8 (j); simplify; intros;
-[1: symmetry; assumption;
-|2: cases (?:False); cases j in H4 H5 H6 H7 H8; intros;
- [1: lapply (q_le_lt_trans ??? H H5) as K;cases (q_lt_corefl ? K);
- |2: lapply (H7 1); [2: do 2 apply le_S_S; apply le_O_n;]
- simplify in Hletin;
- lapply (q_le_lt_trans ??? H Hletin) as K;cases (q_lt_corefl ? K);]]
-qed.
-
-lemma same_values_simpl_to_same_values:
- ∀b1,b2,Hs1,Hs2,Hb1,Hb2,He1,He2,input.
- same_values_simpl b1 b2 →
- value (mk_q_f b1 Hs1 Hb1 He1) input =
- value (mk_q_f b2 Hs2 Hb2 He2) input.
-intros;
-lapply (len_bases_gt_O (mk_q_f b1 Hs1 Hb1 He1));
-lapply (len_bases_gt_O (mk_q_f b2 Hs2 Hb2 He2));
-lapply (H ???? input) as K; try assumption;
-[2: rewrite > Hb1; apply q_pos_OQ;
-|3: rewrite > Hb2; apply q_pos_OQ;
-|1: apply K;]
-qed.
-
-include "russell_support.ma".
-
-lemma value_tail :
- ∀x,y,l,H1,H2,i,H3.
- \fst x < Qpos i →
- value_simpl (y::x::l) H1 H2 i H3 =
- value_simpl (x::l) ?? i ?.
-[1: apply hide; apply (sorted_tail q2_lt); [apply y| assumption]
-|2: apply hide; simplify; apply le_S_S; apply le_O_n;
-|3: apply hide; assumption;]
-intros;cases (cases_value_simpl ? H1 H2 i H3);
-generalize in ⊢ (? ? ? (? ? % ? ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? % ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? ? ? %)); intro;
-cases (cases_value_simpl (x::l) H9 H10 i H11);
-cut (j = S j1) as E; [ destruct E; destruct H12; reflexivity;]
-clear H12 H4; cases j in H8 H5 H6 H7;
-[1: intros;cases (?:False); lapply (H7 1 (le_n ?)); [2: simplify; do 2 apply le_S_S; apply le_O_n]
- simplify in Hletin; apply (q_lt_corefl (\fst x));
- apply (q_lt_le_trans ??? H Hletin);
-|2: simplify; intros; clear q q1 j H11 H10 H1 H2; simplify in H3 H14; apply eq_f;
- cases (cmp_nat n j1); [cases (cmp_nat j1 n);[apply le_to_le_to_eq; assumption]]
- [1: clear H1; cases (?:False);
- lapply (H7 (S j1)); [2: cases j1 in H2; intros[cases (not_le_Sn_O ? H1)] apply le_S_S; assumption]
- [2: apply le_S_S; assumption;] simplify in Hletin;
- apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H13));
- |2: cases (?:False);
- lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption]
- apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]]
-qed.
-
-lemma value_unit:
- ∀x,i,h1,h2,h3.value_simpl [x] h1 h2 i h3 = \snd x.
-intros; cases (cases_value_simpl [x] h1 h2 i h3); cases j in H H2; simplify;
-intros; [2: cases (?:False); apply (not_le_Sn_O n); apply le_S_S_to_le; apply H2]
-symmetry; assumption;
-qed.
-
-lemma same_value_tail:
- ∀b,b1,h1,h3,xs,r1,input,H12,H13,Hi1,H14,H15,Hi2.
- same_values_simpl (〈b1,h1〉::xs) (〈b1,h3〉::r1) →
- value_simpl (b::〈b1,h1〉::xs) H12 H13 input Hi1
- =value_simpl (b::〈b1,h3〉::r1) H14 H15 input Hi2.
-intros; cases (q_cmp (Qpos input) b1);
-[1: rewrite > (value_head 〈b1,h1〉 b xs); [2:assumption]
- rewrite > (value_head 〈b1,h3〉 b r1); [2:assumption] reflexivity;
-|2: rewrite > (value_tail 〈b1,h1〉 b xs);[2: assumption]
- rewrite > (value_tail 〈b1,h3〉 b r1);[2: assumption] apply H;]
-qed.
definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i).
[apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
qed.
+lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a.
+intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭);
+[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;]
+ simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K;
+ simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K);
+|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;]
+ unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin;
+ simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);]
+qed.
+
+lemma value_unit : ∀x,i. value_simple [x] i = \snd x.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) [x] ▭);
+[1: cases i1 in H; intros; [reflexivity] simplify in H;
+ cases (not_le_Sn_O ? (le_S_S_to_le ?? H));
+|2: simplify in H; destruct H; reflexivity;]
+qed.
+lemma value_tail :
+ ∀a,b,l,i.\fst a < Qpos i → \fst b ≤ Qpos i → value_simple (a::b::l) i = value_simple (b::l) i.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) (a::b::l) ▭);
+[1: cases i1 in H3 H2 H4 H5; intros 1; simplify in ⊢ (? ? (? ? %) ?→?); unfold in ⊢ (? ? % ?→?); intros;
+ [1: cases (?:False); cases (q_cmp (Qpos i) (\fst a)) in H3; simplify; intros;[2: destruct H6]
+ apply (q_lt_corefl ? (q_lt_le_trans ??? H H3));
+ |2:
+
+normalize in ⊢ (? ? % ?→?); simplify;
+[1: rewrite > (value_head);
+
lemma value_copy :
- ∀l,h1,h2,i,h3.
- value_simpl (copy l) h1 h2 i h3 = 〈OQ,OQ〉.
-intros; elim l in h1 h2 h3; [cases (not_le_Sn_O ? H1);]
-cases l1 in H H1 H2 H3;
-[1: intros; simplify in ⊢ (? ? (? % ? ? ? ?) ?);
+ ∀l,i.rewrite > (value_u
+ value_simple (copy l) i = 〈OQ,OQ〉.
+intros; elim l;
+[1: reflexivity;
+|2: cases l1 in H; intros; simplify in ⊢ (? ? (? % ?) ?);
+ [1: rewrite > (value_unit); reflexivity;
+ |2: cases (q_cmp (\fst b) (Qpos i));
+
+ change with (\fst ▭ = \lamsimplify in ⊢ (? ? (? % ?) ?); unfold value_simple; unfold match_domain;
+ cases (cases_find bar (match_pred i) [〈\fst x,〈OQ,OQ〉〉] ▭);
+ [1: simplify in H1:(??%%);
+
+ unfold match_pred;
rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity;
|2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?);
cases (q_cmp (Qpos i) (\fst b));
include "russell_support.ma".
include "models/q_copy.ma".
-
+(*
definition rebase_spec ≝
λl1,l2:q_f.λp:q_f × q_f.
And3
whd; rewrite < H6; apply (inversion_sorted2 ??? H5);
| apply (sorted_one q2_lt);]
qed.
+*)
+
+
definition rebase_spec_aux ≝
- λl1,l2:list bar.λp:(list bar) × (list bar).
+ λl1,l2
+ :list bar.λp:(list bar) × (list bar).
sorted q2_lt l1 → (\snd (\last ▭ l1) = 〈OQ,OQ〉) →
sorted q2_lt l2 → (\snd (\last ▭ l2) = 〈OQ,OQ〉) →
rebase_spec_aux_p l1 l2 p.
ous_stuff :> ordered_uniform_space_;
ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
}.
-(*
-definition Type_of_ordered_uniform_space : ordered_uniform_space → Type.
-intro; compose ordered_set_OF_ordered_uniform_space with os_l.
-apply (hos_carr (f o));
-qed.
-
-definition Type_of_ordered_uniform_space_dual : ordered_uniform_space → Type.
-intro; compose ordered_set_OF_ordered_uniform_space with os_r.
-apply (hos_carr (f o));
-qed.
-coercion Type_of_ordered_uniform_space_dual.
-coercion Type_of_ordered_uniform_space.
-*)
definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set.
intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o);
qed.
coercion bs2_of_bss2 nocomposites.
-(*
-notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
-interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
-*)
-
-(*
-lemma ss_of_bs:
- ∀O:ordered_set.∀u,v:O.
- ∀b:O squareO.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} squareO ≝
- λO:ordered_set.λu,v:O.
- λb:O squareB.λH1,H2.〈≪\fst b,H1≫,≪\snd b,H2≫〉.
-*)
-
-(*
-notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
-interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
-*)
-
lemma segment_ordered_uniform_space:
∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
intros (O l r); apply mk_ordered_uniform_space;
alias symbol "pi1" = "exT \fst".
lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀l,u:O.
- ∀x:(segment_ordered_uniform_space O l u).
- ∀a:sequence (segment_ordered_uniform_space O l u).
- uniform_converge (segment_ordered_uniform_space O l u)
- (mk_seq O (λn:nat.\fst (a n))) (\fst x) → True.
+ ∀x:{[l,u]}.
+ ∀a:sequence {[l,u]}.
+ (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) →
a uniform_converges x.
intros 8; cases H1; cases H2; clear H2 H1;
cases (H ? H3) (m Hm); exists [apply m]; intros;
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).
+
+lemma hint_boh1: ∀O. Type_OF_ordered_uniform_space O → hos_carr (os_l O).
+intros; assumption;
+qed.
+
+coercion hint_boh1 nocomposites.
+
+lemma hint_boh2: ∀O:ordered_uniform_space. hos_carr (os_l O) → Type_OF_ordered_uniform_space O.
+intros; assumption;
+qed.
+
+coercion hint_boh2 nocomposites.
+
intros 7;
alias symbol "pi1" (instance 3) = "pair pi1".
alias symbol "pi2" = "pair pi2".
-apply (H (λx:{[l,u]} square.U 〈\fst (\fst x),\fst (\snd x)〉));
+apply (H (λx:{[l,u]} squareB.U 〈\fst (\fst x),\fst (\snd x)〉));
(unfold segment_ordered_uniform_space; simplify);
exists [apply U] split; [assumption;]
intro; cases b; intros; simplify; split; intros; assumption;
qed.
-(* Lemma 3.8 *)
+(* Lemma 3.8 NON DUALIZZATO *)
lemma restrict_uniform_convergence_uparrow:
∀C:ordered_uniform_space.property_sigma C →
∀l,u:C.exhaustive {[l,u]} →
x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫.
intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
[1: split;
- [1: apply (supremum_is_upper_bound C ?? Hx u);
+ [1: apply (supremum_is_upper_bound ? x Hx u);
apply (segment_upperbound ? l);
- |2: apply (le_transitive ? ??? ? (H2 O));
- apply (segment_lowerbound ?l u);]
+ |2: apply (le_transitive l ? x ? (H2 O));
+ apply (segment_lowerbound ? l u a 0);]
|2: intros;
- lapply (uparrow_upperlocated ? a ≪x,h≫) as Ha1;
- [2: apply segment_preserves_uparrow;split; assumption;]
- lapply (segment_preserves_supremum ? l u a ≪?,h≫) as Ha2;
+ 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;
[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); [left; split; assumption]
apply restric_uniform_convergence; assumption;]
qed.
-
-lemma restrict_uniform_convergence_downarrow:
+
+lemma hint_mah1:
+ ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
+ intros; assumption; qed.
+
+coercion hint_mah1 nocomposites.
+
+lemma hint_mah2:
+ ∀C. sequence (hos_carr (os_l C)) → sequence (hos_carr (os_r C)).
+ intros; assumption; qed.
+
+coercion hint_mah2 nocomposites.
+
+lemma hint_mah3:
+ ∀C. Type_OF_ordered_uniform_space C → hos_carr (os_r C).
+ intros; assumption; qed.
+
+coercion hint_mah3 nocomposites.
+
+lemma hint_mah4:
+ ∀C. sequence (hos_carr (os_r C)) → sequence (hos_carr (os_l C)).
+ intros; assumption; qed.
+
+coercion hint_mah4 nocomposites.
+
+axiom 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 →
+ ∀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 C ?? Hx l);
+ [2: apply (infimum_is_lower_bound ? x Hx l);
apply (segment_lowerbound ? l u);
- |1: apply (le_transitive ???? (H2 O));
- apply (segment_upperbound ? l u);]
+ |1: lapply (ge_transitive ? ? x ? (H2 O)); [apply u||assumption]
+ apply (segment_upperbound ? l u a 0);]
|2: intros;
- lapply (downarrow_lowerlocated ? a ≪x,h≫) as Ha1;
- [2: apply segment_preserves_downarrow;split; assumption;]
- lapply (segment_preserves_infimum ?l u a ≪?,h≫) as Ha2;
+ 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: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
+qed.
+*)
\ No newline at end of file
definition property_sigma ≝
λC:ordered_uniform_space.
∀U.us_unifbase ? U →
- ∃V:sequence (C square → Prop).
+ ∃V:sequence (C squareB → Prop).
(∀i.us_unifbase ? (V i)) ∧
∀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〉.
lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
intros; rewrite > sym_max in H; apply (max_le_l ??? H);
qed.
-
+
(* Lemma 3.6 *)
lemma sigma_cauchy:
∀C:ordered_uniform_space.property_sigma C →
clearbody m; unfold spec in m Hm Hm1; clear spec;
cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,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);]]
+ [ 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;
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);]]
+ simplify; repeat split;
+ [1,6: apply (le_reflexive l);
+ |2,5: apply (H12 (\fst (m 0)));
+ |3,8: apply (H12 i);
+ |4:change with (a (m O) ≤ a i);
+ apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H14);
+ |7:change with (a i ≤ a (m O));
+ apply (trans_decreasing ? H6 (\fst (m 0)) i); 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));
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;]
+[1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p q H4);
-|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
+|2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p r H5);]
qed.
[1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
|2: apply Hmb; apply (le_w_plus ma); assumption]
- |2: simplify; apply (le_transitive ???? Lax Lxb);
+ |2: simplify; apply (le_transitive (a i) ?? Lax Lxb);
|3: simplify; repeat split; try assumption;
- [1: apply (le_transitive ???? Lax Lxb);
- |2: intro X; cases (os_coreflexive ?? X)]]
+ [1: apply (le_transitive ?? (b i) Lax Lxb);
+ |2: intro X; cases (exc_coreflexive (a i) X)]]
|1: apply HW; exists[apply l] simplify; split;
[1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
|2: apply Hma; rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]
projects / helm.git / commitdiff