notation "hvbox(a break # b)" non associative with precedence 45
for @{ 'apart $a $b}.
-interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y).
+interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
definition bishop_set_of_ordered_set: ordered_set → bishop_set.
intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));
intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
assumption;
qed.
+
+definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+interpretation "bishop set subset" 'subset a b = (bs_subset _ a b).
+
+definition square_bishop_set : bishop_set → bishop_set.
+intro S; apply (mk_bishop_set (S × S));
+[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
+|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
+|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
+|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
+ [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
+ |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
+qed.
+
+notation "s 2 \atop \neq" non associative with precedence 90
+ for @{ 'square_bs $s }.
+interpretation "bishop set square" 'square x = (square_bishop_set x).
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file
interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
+coinductive product (A,B:Type) : Type ≝ pair : ∀a:A.∀b:B.product A B.
+
+notation "a \times b" left associative with precedence 70 for @{'product $a $b}.
+interpretation "prod" 'product a b = (product a b).
+
+definition first : ∀A.∀P.A × P → A ≝ λA,P,s.match s with [pair x _ ⇒ x].
+definition second : ∀A.∀P.A × P → P ≝ λA,P,s.match s with [pair _ y ⇒ y].
+
+interpretation "pair pi1" 'pi1 = (first _ _).
+interpretation "pair pi2" 'pi2 = (second _ _).
+interpretation "pair pi1" 'pi1a x = (first _ _ x).
+interpretation "pair pi2" 'pi2a x = (second _ _ x).
+interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
+interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
+
+notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
+interpretation "pair" 'pair a b = (pair _ _ a b).
+
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.
+interpretation "dependent pair" 'pair a b = (ex_introT _ _ a b).
notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}.
notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}.
interpretation "exT snd" 'pi2a x = (pi2exT _ _ x).
interpretation "exT snd" 'pi2b x y = (pi2exT _ _ x y).
+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.
+
definition pi1exT23 ≝
λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
definition pi2exT23 ≝
definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
-
-sandwich.ma ordered_uniform.ma
property_sigma.ma ordered_uniform.ma russell_support.ma
-uniform.ma supremum.ma
bishop_set.ma ordered_set.ma
-sequence.ma nat/nat.ma
ordered_uniform.ma uniform.ma
-supremum.ma bishop_set.ma cprop_connectives.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
-property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
bishop_set_rewrite.ma bishop_set.ma
-cprop_connectives.ma logic/equality.ma
-nat_ordered_set.ma ordered_set.ma bishop_set.ma cprop_connectives.ma nat/compare.ma
+sequence.ma nat/nat.ma
+nat_ordered_set.ma bishop_set.ma nat/compare.ma
lebesgue.ma property_exhaustivity.ma sandwich.ma
+property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
+cprop_connectives.ma logic/equality.ma
ordered_set.ma cprop_connectives.ma
+sandwich.ma ordered_uniform.ma
russell_support.ma cprop_connectives.ma nat/nat.ma
+uniform.ma supremum.ma
+supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
models/uniformnat.ma bishop_set_rewrite.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma
datatypes/constructors.ma
logic/equality.ma
∀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 ≤ (fst p) j.
+ ∀j.l ≤ (pi1exT23 ???? p) j.
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;
∀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.
+ ∀j.(pi2exT23 ???? 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);
∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
∀x:C.a order_converges x →
x ∈ [l,u] ∧
- ∀h:x ∈ [l,u]. (* manca il pullback? *)
- uniform_converge
- (uniform_space_OF_ordered_uniform_space
- (segment_ordered_uniform_space C l u))
- (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
- (sig_in ?? x h).
+ ∀h:x ∈ [l,u].
+ uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
intros;
generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
[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;
+ letin Xi ≝ (⌊n,〈xi n,Hxi n〉⌋);
+ letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋);
+ letin Ai ≝ (⌊n,〈a n,H1 n〉⌋);
+ apply (sandwich {[l,u]} 〈?,h〉 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;]
+ |2: cases (H l u Xi 〈?,h〉) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
exists [apply w] apply H7;
- |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+ |3: cases (H l u Yi 〈?,h〉) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
exists [apply w] apply H7;]]
qed.
∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
∀x:C.a order_converges x →
x ∈ [l,u] ∧
- ∀h:x ∈ [l,u]. (* manca il pullback? *)
- uniform_converge
- (uniform_space_OF_ordered_uniform_space
- (segment_ordered_uniform_space C l u))
- (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
- (sig_in ?? x h).
+ ∀h:x ∈ [l,u].
+ uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
intros (C S);
generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
|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;
+ letin Xi ≝ (⌊n,〈xi n,Hxi n〉⌋);
+ letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋);
+ letin Ai ≝ (⌊n,〈a n,H1 n〉⌋);
+ apply (sandwich {[l,u]} 〈x,h〉 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);
definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
intro C; apply (mk_uniform_space C);
[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
-|2: intros 4 (U H x Hx); unfold in Hx;
+|2: intros 4 (U H x Hx); simplify in Hx;
cases H (_ H1); cases (H1 x); apply H2; apply Hx;
|3: intros; cases H (_ PU); cases H1 (_ PV);
exists[apply (λx.U x ∧ V x)] split;
[1: exists[apply something] intro; cases (PU n); cases (PV n);
split; intros; try split;[apply H2;|apply H4] try assumption;
apply H3; cases H6; assumption;
- |2: simplify; unfold mk_set; intros; assumption;]
+ |2: simplify; intros; assumption;]
|4: intros; cases H (_ PU); exists [apply U] split;
[1: exists [apply something] intro n; cases (PU n);
split; intros; try split;[apply H1;|apply H2] assumption;
cases Hcut1; assumption]
qed.
-alias symbol "pi1" = "sigma pi1".
+alias symbol "pi1" = "exT fst".
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs);
+intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉);
fold normalize X; intros; cases H1;
-alias symbol "pi1" = "sigma pi1".
letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
letin m ≝ (
let rec aux i ≝
apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
apply(trans_increasing ?? H (S n2) (pred) H77);]]]]]
clearbody m; unfold spec in m; clear spec;
-cut (∀i.fst a (m i) = s ∨ i ≤ fst (a (m i))) as key2;[
+cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[
letin find ≝ (
let rec find i u on u : nat ≝
match u with
cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
cases (Lb1b H1);
qed.
+
+lemma square_ordered_set: ordered_set → ordered_set.
+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);
+|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
+ clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
+ [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_os $s }.
+notation > "s 'square'" non associative with precedence 90
+ for @{ 'square $s }.
+interpretation "ordered set square" 'square s = (square_ordered_set s).
+interpretation "ordered set square" 'square_os s = (square_ordered_set s).
+
+definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+notation "a \subseteq u" left associative with precedence 70
+ for @{ 'subset $a $u }.
+interpretation "ordered set subset" 'subset a b = (os_subset _ a b).
+
ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
}.
-lemma segment_square_of_O_square:
+definition invert_os_relation ≝
+ λC:ordered_set.λU:C square → Prop.
+ λx:C square. U 〈snd x,fst x〉.
+
+interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+
+lemma segment_square_of_ordered_set_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.
+coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2.
-alias symbol "pi1" (instance 4) = "sigma pi1".
-alias symbol "pi1" (instance 2) = "sigma pi1".
-lemma O_square_of_segment_square :
+alias symbol "pi1" (instance 4) = "exT fst".
+alias symbol "pi1" (instance 2) = "exT fst".
+lemma ordered_set_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)〉.
+ λ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.
+coercion cic:/matita/dama/ordered_uniform/ordered_set_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));
+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;
+intros 7; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b b1 x;
+cases (H 〈w1,w2〉 H1 H2) (L _); intro Uw; apply L; apply Uw;
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;
+intros 6; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b1 b x;
+intros (Ra uw); cases (Ra 〈w1,w2〉 H1 H2) (_ R); apply R; apply uw;
qed.
lemma invert_restriction_agreement:
- ∀O:ordered_uniform_space.∀l,r:O.∀U:{[l,r]} square → Prop.∀u.
+ ∀O:ordered_uniform_space.∀l,r:O.
+ ∀U:{[l,r]} square → Prop.∀u:O square → Prop.
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);]
+[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);
+|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);]
qed.
+alias symbol "square" (instance 8) = "bishop set square".
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)〉.
+ λ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}.
+notation < "x \sub \neq" left associative with precedence 91 for @{'bsss $x}.
interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
+alias symbol "square" (instance 7) = "ordered set square".
+alias symbol "pair" (instance 4) = "dependent pair".
+alias symbol "pair" (instance 2) = "dependent pair".
+lemma ss_of_bs:
+ ∀O:ordered_set.∀u,v:O.
+ ∀b:O square.fst b ∈ [u,v] → snd b ∈ [u,v] → {[u,v]} square ≝
+ λO:ordered_set.λu,v:O.
+ λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉.
+
+notation < "x \sub \nleq" left associative 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;
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;
+ [1: intros (U H); intro x; 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);
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; (* ??? *)
+ unfold segment_square_of_ordered_set_square;
cases b; intros; split; intros; assumption;
- |2: intros 2 (x Hx); unfold mk_set; cases (Hw ? Hx); split;
+ |2: intros 2 (x Hx); 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; (* ??? *)
+ unfold segment_square_of_ordered_set_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));
+ [1: lapply (invert_restriction_agreement ????? HuU) as Ra;
+ apply (restrict ????? x Ra);
apply Hul; apply (unrestrict ?????? HuU H);
|2: apply (restrict ?????? HuU); apply Hur;
apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]]
(segment_ordered_uniform_space _ a b).
(* Lemma 3.2 *)
-alias symbol "pi1" = "sigma pi1".
+alias symbol "pi1" = "exT fst".
lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀l,u:O.
∀x:{[l,u]}.
∀a:sequence {[l,u]}.
- (λn.fst (a n)) uniform_converges (fst x) →
+ ⌊n,fst (a n)⌋ 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;
(b is_decreasing → b is_lower_located → b is_cauchy).
lemma segment_upperbound:
- ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound (λn.fst (a n)).
+ ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,fst (a n)⌋.
intros 5; change with (fst (a n) ≤ u); cases (a n); cases H; assumption;
qed.
lemma segment_lowerbound:
- ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound (λn.fst (a n)).
+ ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,fst (a n)⌋.
intros 5; change with (l ≤ fst (a n)); cases (a n); cases H; assumption;
qed.
lemma segment_preserves_uparrow:
∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h.
- (λn.fst (a n)) ↑ x → a ↑ (sig_in ?? x h).
+ ⌊n,fst (a n)⌋ ↑ x → a ↑ 〈x,h〉.
intros; cases H (Ha Hx); split [apply Ha] cases Hx;
split; [apply H1] intros;
cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption;
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).
+ ⌊n,fst (a n)⌋ ↓ x → a ↓ 〈x,h〉.
intros; cases H (Ha Hx); split [apply Ha] cases Hx;
split; [apply H1] intros;
cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption;
(* Fact 2.18 *)
lemma segment_cauchy:
∀C:ordered_uniform_space.∀l,u:C.∀a:sequence {[l,u]}.
- a is_cauchy → (λn:nat.fst (a n)) is_cauchy.
+ a is_cauchy → ⌊n,fst (a n)⌋ is_cauchy.
intros 7;
alias symbol "pi1" (instance 3) = "pair pi1".
alias symbol "pi2" = "pair pi2".
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 →
- x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h).
+ ∀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;
[1: apply (supremum_is_upper_bound C ?? Hx u);
apply (segment_upperbound ? l);
- |2: apply (le_transitive ?? (fst (a 0))); [2: apply H2;]
+ |2: apply (le_transitive ? ??? ? (H2 O));
apply (segment_lowerbound ?l u);]
|2: intros;
- lapply (uparrow_upperlocated ? a (sig_in ?? x h)) as Ha1;
+ lapply (uparrow_upperlocated ? a 〈x,h〉) as Ha1;
[2: apply segment_preserves_uparrow;split; assumption;]
- lapply (segment_preserves_supremum ?l u a (sig_in ??? h)) as Ha2;
+ 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;
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).
+ ∀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);
apply (segment_lowerbound ? l u);
- |1: apply (le_transitive ?? (fst (a 0))); [apply H2;]
+ |1: apply (le_transitive ???? (H2 O));
apply (segment_upperbound ? l u);]
|2: intros;
- lapply (downarrow_lowerlocated ? a (sig_in ?? x h)) as Ha1;
+ lapply (downarrow_lowerlocated ? a 〈x,h〉) as Ha1;
[2: apply segment_preserves_downarrow;split; assumption;]
- lapply (segment_preserves_infimum ?l u a (sig_in ??? h)) as Ha2;
+ lapply (segment_preserves_infimum ?l u 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;
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 →
∀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;
+alias symbol "pair" = "pair".
+letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
match i with
[ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
| S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
] in aux
- :
- ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
+ : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
[1,2:apply H8;
|3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
simplify in ⊢ (?→? (? % ?) ?→?);
apply lt_to_le; apply (max_le_r w1); 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:
+cut ((⌊x,(m x: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)));]
-cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
intro n; intro L; change in L with (m (S n) < 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;
-cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2:
+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 associative with precedence 70
for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
+notation > "hvbox((\lfloor p \rfloor) \sub ident i)"
+ left associative with precedence 70
+for @{ 'sequence (\lambda ${ident i} . $p)}.
+
notation > "hvbox(\lfloor ident i, p \rfloor)"
left associative with precedence 70
for @{ 'sequence (\lambda ${ident i} . $p)}.
for @{'segment_in $a $b $x}.
interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
-(*
-coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
-
-definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
-
-interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x).
-
-interpretation "Type exists" 'exists \eta.x = (sigma _ x).
-*)
-
lemma segment_ordered_set:
∀O:ordered_set.∀u,v:O.ordered_set.
intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
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].
-definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 = (first _ _).
-interpretation "pair pi2" 'pi2 = (second _ _).
-interpretation "pair pi1" 'pi1a x = (first _ _ x).
-interpretation "pair pi2" 'pi2a x = (second _ _ x).
-interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
-interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
-
-notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b = (prod _ _ a b).
-interpretation "prod" 'product a b = (pair a b).
-
-lemma square_ordered_set: ordered_set → ordered_set.
-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);
-|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
- clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
- [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 = (square_ordered_set s).
-
+alias symbol "square" = "ordered set square".
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
definition square_segment ≝
- λO:ordered_set.λa,b:O.λx:square_ordered_set O.
+ λO:ordered_set.λa,b:O.λx:O square.
And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
definition convex ≝
include "supremum.ma".
-(* Definition 2.13 *)
-definition square_bishop_set : bishop_set → bishop_set.
-intro S; apply (mk_bishop_set (pair S S));
-[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
-|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
-|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
-|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
- [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
- |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
-qed.
-
-definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-notation "a \subseteq u" left associative with precedence 70
- for @{ 'subset $a $u }.
-interpretation "Bishop subset" 'subset a b = (subset _ a b).
-
-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 set square" 'square x = (square_bishop_set x).
-interpretation "bishop set square" 'square2 x = (square_bishop_set x).
+(* Definition 2.13 *)
+alias symbol "square" = "bishop set square".
+alias symbol "pair" = "pair".
alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
-definition compose_relations ≝
+definition compose_bs_relations ≝
λC:bishop_set.λU,V:C square → Prop.
λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
-notation "a \circ b" left associative with precedence 70
- for @{'compose $a $b}.
-interpretation "relations composition" 'compose a b = (compose_relations _ a b).
+definition compose_os_relations ≝
+ λC:ordered_set.λU,V:C square → Prop.
+ λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+
+interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
+interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
-definition invert_relation ≝
+definition invert_bs_relation ≝
λC:bishop_set.λU:C square → Prop.
λx:C square. U 〈snd x,fst x〉.
notation < "s \sup (-1)" left associative with precedence 70
for @{ 'invert $s }.
notation < "s \sup (-1) x" left associative with precedence 70
- for @{ 'invert2 $s $x}.
+ for @{ 'invert_appl $s $x}.
notation > "'inv'" right associative with precedence 70
- for @{ 'invert0 }.
-interpretation "relation invertion" 'invert a = (invert_relation _ a).
-interpretation "relation invertion" 'invert0 = (invert_relation _).
-interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
+ for @{ 'invert_symbol }.
+interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
+interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
+interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
alias symbol "exists" = "CProp exists".
+alias symbol "compose" = "bishop set relations composition".
alias symbol "and" (instance 21) = "constructive and".
alias symbol "and" (instance 16) = "constructive and".
alias symbol "and" (instance 9) = "constructive and".
projects / helm.git / commitdiff