inductive exT (A:Type) (P:A→CProp) : CProp ≝
ex_introT: ∀w:A. P w → exT A P.
+record sigT (A:Type) (P:A→CProp) : Type ≝ {
+ fstT:A;
+ sndT:P fstT
+}.
+
+interpretation "sigT \fst" 'pi1 = (fstT _ _).
+interpretation "sigT \fst" 'pi1a x = (fstT _ _ x).
+interpretation "sigT \fst" 'pi1b x y = (fstT _ _ x y).
+interpretation "sigT \snd" 'pi2 = (sndT _ _).
+interpretation "sigT \snd" 'pi2a x = (sndT _ _ x).
+interpretation "sigT \snd" 'pi2b x y = (sndT _ _ x y).
+
+notation "\ll term 19 a, break term 19 b \gg"
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b =
+ (ex_introT _ _ a b).
+
+interpretation "dependent set" 'dependent_pair a b =
+ (mk_sigT _ _ a b).
+
interpretation "CProp exists" 'exists \eta.x = (exT _ x).
notation "\ll term 19 a, break term 19 b \gg"
intro H2; cases (H10 ? H2);
cases (H (w1+j)); apply (H11 H7);
qed.
-
+
(* Theorem 3.10 *)
theorem lebesgue_oc:
∀C:ordered_uniform_space.
[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 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;
+ letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
+ letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
+ letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
+ apply (sandwich {[l,u]} (mk_sigT ?? 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 (H l u Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
|2: intros 3;
lapply (uparrow_upperlocated ? xi x Hx)as Ux;
lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
- 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;
+ letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
+ letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
+ letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
+ apply (sandwich {[l,u]} (mk_sigT ?? 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);
alias symbol "pi2" = "pair pi2".
alias symbol "pi1" = "pair pi1".
alias symbol "and" = "logical and".
- apply (∃_:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n));
+ apply (∃d:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n));
|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);
coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2.
-alias symbol "pi1" (instance 4) = "exT \fst".
-alias symbol "pi1" (instance 2) = "exT \fst".
+alias symbol "pi1" (instance 4) = "sigT \fst".
+alias symbol "pi1" (instance 2) = "sigT \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)〉.
interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
alias symbol "square" (instance 7) = "ordered set square".
+alias symbol "square" (instance 13) = "ordered set square".
+alias symbol "dependent_pair" = "dependent set".
lemma ss_of_bs:
∀O:ordered_set.∀u,v:O.
∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝
(segment_ordered_uniform_space _ a b).
(* Lemma 3.2 *)
-alias symbol "pi1" = "exT \fst".
+alias symbol "pi1" = "sigT \fst".
lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀l,u:O.
∀x:{[l,u]}.
interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
(* Definition 2.8 *)
-alias symbol "and" = "constructive and".
definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
lemma segment_ordered_set:
∀O:ordered_set.∀u,v:O.ordered_set.
-intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
+intros (O u v); apply (mk_ordered_set (sigT ? (λx.x ∈ [u,v])));
[1: intros (x y); apply (\fst x ≰ \fst y);
|2: intro x; cases x; simplify; apply os_coreflexive;
|3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]