uniform.ma supremum.ma
supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
+ordered_uniform.ma uniform.ma
+sandwich.ma ordered_uniform.ma
logic/equality.ma
nat/compare.ma
nat/nat.ma
record ordered_uniform_space : Type ≝ {
ous_stuff :> ordered_uniform_space_;
- ous_prop1: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
-}.
+ ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
+}.
+
+lemma segment_square_of_O_square:
+ ∀O:ordered_set.∀u,v:O.∀x:O square.fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square.
+intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption;
+qed.
+
+coercion cic:/matita/dama/ordered_uniform/segment_square_of_O_square.con 0 2.
+alias symbol "pi1" (instance 4) = "sigma pi1".
+alias symbol "pi1" (instance 2) = "sigma pi1".
+lemma O_square_of_segment_square :
+ ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝
+ λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+
+coercion cic:/matita/dama/ordered_uniform/O_square_of_segment_square.con.
+
+lemma restriction_agreement :
+ ∀O:ordered_uniform_space.∀l,r:O.∀P:{[l,r]} square → Prop.∀OP:O square → Prop.Prop.
+apply(λO:ordered_uniform_space.λl,r:O.λP:{[l,r]} square → Prop.λOP:O square → Prop.
+ ∀b:O square.∀H1,H2.
+ (P b → OP b) ∧ (OP b → P b));
+[5,7: apply H1|6,8:apply H2]skip;
+qed.
+
+lemma unrestrict: ∀O:ordered_uniform_space.∀l,r:O.∀U,u.∀x:{[l,r]} square.
+ restriction_agreement ? l r U u → U x → u x.
+intros 7; cases x (b b1); cases b; cases b1;
+cases (H 〈x1,x2〉 H1 H2) (L _); intros; apply L; assumption;
+qed.
+
+lemma restrict: ∀O:ordered_uniform_space.∀l,r:O.∀U,u.∀x:{[l,r]} square.
+ restriction_agreement ? l r U u → u x → U x.
+intros 6; cases x (b b1); cases b; cases b1; intros (X);
+cases (X 〈x1,x2〉 H H1) (_ R); apply R; assumption;
+qed.
+
+lemma invert_restriction_agreement:
+ ∀O:ordered_uniform_space.∀l,r:O.∀U:{[l,r]} square → Prop.∀u.
+ restriction_agreement ? l r U u →
+ restriction_agreement ? l r (inv U) (inv u).
+intros 9; split; intro;
+[1: apply (unrestrict ????? (segment_square_of_O_square ??? 〈snd b,fst b〉 H2 H1) H H3);
+|2: apply (restrict ????? (segment_square_of_O_square ??? 〈snd b,fst b〉 H2 H1) H H3);]
+qed.
+
+lemma bs_of_ss:
+ ∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝
+ λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+
+notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
+interpretation "bs_of_ss" 'bsss x =
+ (cic:/matita/dama/ordered_uniform/bs_of_ss.con _ _ _ x).
lemma segment_ordered_uniform_space:
∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
-intros (O u v); apply mk_ordered_uniform_space;
-[1: apply mk_ordered_uniform_space_;
- [1: apply (mk_ordered_set (sigma ? (λx.x ∈ [u,v])));
- [1: intros (x y); apply (fst x ≰ fst y);
- |2: intros 1; cases x; simplify; apply os_coreflexive;
- |3: intros 3; cases x; cases y; cases z; simplify; apply os_cotransitive]
- |2: apply (mk_uniform_space (bishop_set_of_ordered_set (mk_ordered_set (sigma ? (λx.x ∈ [u,v])) ???)));
- |3: apply refl_eq;
+intros (O l r); apply mk_ordered_uniform_space;
+[1: apply (mk_ordered_uniform_space_ {[l,r]});
+ [1: alias symbol "and" = "constructive and".
+ letin f ≝ (λP:{[l,r]} square → Prop. ∃OP:O square → Prop.
+ (us_unifbase O OP) ∧ restriction_agreement ??? P OP);
+ apply (mk_uniform_space (bishop_set_of_ordered_set {[l,r]}) f);
+ [1: intros (U H); intro x; unfold mk_set; simplify;
+ cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm;
+ lapply (us_phi1 ?? Gw x Hm) as IH;
+ apply (restrict ?????? Hwp IH);
+ |2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV;
+ cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv;
+ cases (us_phi2 ??? Gu Gv) (w HW); cases HW (Gw Hw); clear HW;
+ exists; [apply (λb:{[l,r]} square.w b)] split;
+ [1: unfold f; simplify; clearbody f;
+ exists; [apply w]; split; [assumption] intro b; simplify;
+ unfold segment_square_of_O_square; (* ??? *)
+ cases b; intros; split; intros; assumption;
+ |2: intros 2 (x Hx); unfold mk_set; cases (Hw ? Hx); split;
+ [apply (restrict ?????? HuU H)|apply (restrict ?????? HvV H1);]]
+ |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU;
+ cases (us_phi3 ?? Gu) (w HW); cases HW (Gw Hwu); clear HW;
+ exists; [apply (λx:{[l,r]} square.w x)] split;
+ [1: exists;[apply w];split;[assumption] intros; simplify; intro;
+ unfold segment_square_of_O_square; (* ??? *)
+ cases b; intros; split; intro; assumption;
+ |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu;
+ cases Hx (m Hm); exists[apply (fst m)] apply Hm;]
+ |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu;
+ cases (us_phi4 ?? Gu x) (Hul Hur);
+ split; intros;
+ [1: apply (restrict ?????? (invert_restriction_agreement ????? HuU));
+ apply Hul; apply (unrestrict ?????? HuU H);
+ |2: apply (restrict ?????? HuU); apply Hur;
+ apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]]
+ |2: simplify; reflexivity;]
+|2: simplify; unfold convex; intros;
+ cases H (u HU); cases HU (Gu HuU); clear HU H;
+ lapply (ous_convex ?? Gu (bs_of_ss ? l r p) ? H2 (bs_of_ss ? l r y) H3) as Cu;
+ [1: apply (unrestrict ?????? HuU); apply H1;
+ |2: apply (restrict ?????? HuU Cu);]]
qed.
+interpretation "Ordered uniform space segment" 'segment_set a b =
+ (cic:/matita/dama/ordered_uniform/segment_ordered_uniform_space.con _ a b).
(* Lemma 3.2 *)
+alias symbol "pi1" = "sigma pi1".
lemma foo:
∀O:ordered_uniform_space.∀l,u:O.
- ∀x:(segment_ordered_uniform_space O l u).
- ∀a:sequence (segment_ordered_uniform_space O l u).
- (* (λn.fst (a n)) uniform_converges (fst x) → *)
+ ∀x:{[l,u]}.
+ ∀a:sequence {[l,u]}.
+ (λn.fst (a n)) uniform_converges (fst x) →
a uniform_converges x.
-
-
\ No newline at end of file
+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.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ordered_uniform.ma".
+
+lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o.
+intro; elim n; simplify; [assumption]
+lapply (le_S ?? H1); apply H; apply le_S_S_to_le; assumption;
+qed.
+
+alias symbol "leq" = "Ordered set less or equal than".
+alias symbol "and" = "logical and".
+theorem sandwich:
+ ∀O:ordered_uniform_space.∀l:O.∀a,b,x:sequence O.
+ (∀i:nat.a i ≤ x i ∧ x i ≤ b i) →
+ a uniform_converges l →
+ b uniform_converges l →
+ x uniform_converges l.
+intros 10;
+cases (us_phi3 ? ? H3) (V GV); cases GV (Gv HV); clear GV;
+cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW;
+cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
+exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉);
+unfold; simplify; exists [apply (a i)] split;
+[2: apply (ous_convex ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
+ [1: apply HW; exists [apply l]simplify; split;
+ [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);
+ |3: simplify; repeat split; try assumption;
+ [1: apply (le_transitive ???? Lax Lxb);
+ |2: (* prove le_reflexive *) intro X; cases (os_coreflexive ?? 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;]]
+qed.
+
interpretation "Ordered set sergment" 'segment a b =
(cic:/matita/dama/supremum/segment.con _ a b).
-notation "x \in [a,b]" non associative with precedence 50
+notation "hvbox(x \in break [a,b])" non associative with precedence 50
for @{'segment2 $a $b $x}.
interpretation "Ordered set sergment in" 'segment2 a b x=
(cic:/matita/dama/supremum/segment.con _ a b x).
definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
-notation < "\pi \sub 1 x" non associative with precedence 50 for @{'pi1 $x}.
-notation < "\pi \sub 2 x" non associative with precedence 50 for @{'pi2 $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 =
(cic:/matita/dama/supremum/pi1.con _ _ x).
-
+
interpretation "Type exists" 'exists \eta.x =
(cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
|3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
qed.
-notation < "{\x|\x \in [a,b]}" non associative with precedence 90
+notation "hvbox({[a, break b]})" non associative with precedence 90
for @{'segment_set $a $b}.
interpretation "Ordered set segment" 'segment_set a b =
(cic:/matita/dama/supremum/segment_ordered_set.con _ a b).
(* Lemma 2.9 *)
lemma segment_preserves_supremum:
- ∀O:ordered_set.∀l,u:O.∀a:sequence (segment_ordered_set ? l u).
- ∀x:(segment_ordered_set ? l u).
+ ∀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;
(cic:/matita/dama/supremum/first.con _ _ x).
interpretation "pair pi2" 'pi2 x =
(cic:/matita/dama/supremum/second.con _ _ x).
+
+notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
+interpretation "pair" 'pair a b =
+ (cic:/matita/dama/supremum/pair.ind#xpointer(1/1/1) _ _ a b).
+
+notation "a \times b" left associative with precedence 60 for @{'prod $a $b}.
+interpretation "prod" 'prod a b =
+ (cic:/matita/dama/supremum/pair.ind#xpointer(1/1) a b).
lemma square_ordered_set: ordered_set → ordered_set.
-intro O; apply (mk_ordered_set (pair O O));
+intro O; apply (mk_ordered_set (O × O));
[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
cases H (X X); apply (os_coreflexive ?? X);
[1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
|2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
qed.
+
+notation < "s 2 \atop \nleq" non associative with precedence 90
+ for @{ 'square $s }.
+notation > "s 'square'" non associative with precedence 90
+ for @{ 'square $s }.
+interpretation "ordered set square" 'square s =
+ (cic:/matita/dama/supremum/square_ordered_set.con s).
definition square_segment ≝
λO:ordered_set.λa,b:O.λx:square_ordered_set O.
(cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))).
definition convex ≝
- λO:ordered_set.λU:square_ordered_set O → Prop.
+ λO:ordered_set.λU:O square → Prop.
∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
(* Definition 2.11 *)
interpretation "Bishop subset" 'subset a b =
(cic:/matita/dama/uniform/subset.con _ a b).
-notation "{ ident x : t | p }" non associative with precedence 50
+notation "hvbox({ ident x : t | break p })" non associative with precedence 50
for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.
definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
interpretation "explicit set" 'explicitset t =
(cic:/matita/dama/uniform/mk_set.con _ t).
-notation < "s \sup 2" non associative with precedence 90
- for @{ 'square $s }.
+notation < "s 2 \atop \neq" non associative with precedence 90
+ for @{ 'square2 $s }.
notation > "s 'square'" non associative with precedence 90
for @{ 'square $s }.
-interpretation "bishop suqare set" 'square x =
+interpretation "bishop set square" 'square x =
+ (cic:/matita/dama/uniform/square_bishop_set.con x).
+interpretation "bishop set square" 'square2 x =
(cic:/matita/dama/uniform/square_bishop_set.con x).
+
alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
definition compose_relations ≝
λC:bishop_set.λU,V:C square → Prop.
- λx:C square.∃y:C. U (prod ?? (fst x) y) ∧ V (prod ?? y (snd x)).
+ λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
notation "a \circ b" left associative with precedence 60
for @{'compose $a $b}.
interpretation "relations composition" 'compose a b =
(cic:/matita/dama/uniform/compose_relations.con _ a b).
+notation "hvbox(x \in break a \circ break b)" non associative with precedence 50
+ for @{'compose2 $a $b $x}.
+interpretation "relations composition" 'compose2 a b x =
+ (cic:/matita/dama/uniform/compose_relations.con _ a b x).
definition invert_relation ≝
λC:bishop_set.λU:C square → Prop.
- λx:C square. U (prod ?? (snd x) (fst x)).
+ λx:C square. U 〈snd x,fst x〉.
notation < "s \sup (-1)" non associative with precedence 90
for @{ 'invert $s }.
+notation < "s \sup (-1) x" non associative with precedence 90
+ for @{ 'invert2 $s $x}.
notation > "'inv' s" non associative with precedence 90
for @{ 'invert $s }.
interpretation "relation invertion" 'invert a =
(cic:/matita/dama/uniform/invert_relation.con _ a).
+interpretation "relation invertion" 'invert2 a x =
+ (cic:/matita/dama/uniform/invert_relation.con _ a x).
+alias symbol "exists" = "CProp exists".
+alias symbol "and" (instance 18) = "constructive and".
+alias symbol "and" (instance 10) = "constructive and".
record uniform_space : Type ≝ {
us_carr:> bishop_set;
us_unifbase: (us_carr square → Prop) → CProp;
∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
- us_phi4: ∀U:us_carr square → Prop. us_unifbase U → U = inv U (* I should use double inclusion ... *)
+ us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
}.
(* Definition 2.14 *)
alias symbol "leq" = "natural 'less or equal to'".
definition cauchy ≝
λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
- ∃n. ∀i,j. n ≤ i → n ≤ j → U (prod ?? (a i) (a j)).
+ ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
for @{'cauchy $a}.
(* Definition 2.15 *)
definition uniform_converge ≝
λC:uniform_space.λa:sequence C.λu:C.
- ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U (prod ?? u (a i)).
+ ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉.
notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
for @{'uniform_converge $a $x}.
cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
-rewrite > (us_phi4 ?? Hv); simplify; apply (Hn ? H1);
+cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
+apply (Hn ? H1);
qed.
(* Definition 2.17 *)
projects / helm.git / commitdiff