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 =
- (cic:/matita/dama/uniform/subset.con _ a b).
-
-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 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 =
- (cic:/matita/dama/uniform/square_bishop_set.con x).
-interpretation "bishop set square" 'square2 x =
- (cic:/matita/dama/uniform/square_bishop_set.con 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 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 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)" 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).
+notation < "s \sup (-1)" with precedence 70 for @{ 'invert $s }.
+notation < "s \sup (-1) x" with precedence 70
+ for @{ 'invert_appl $s $x}.
+notation > "'inv'" with precedence 70 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 "and" (instance 18) = "constructive and".
-alias symbol "and" (instance 10) = "constructive and".
+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".
record uniform_space : Type ≝ {
us_carr:> bishop_set;
us_unifbase: (us_carr square → Prop) → CProp;
us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
- {x:us_carr square|fst x ≈ snd x} ⊆ U;
+ (λx:us_carr square.fst x ≈ snd x) ⊆ U;
us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
- ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
+ ∃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 → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
for @{'cauchy $a}.
notation > "a 'is_cauchy'" non associative with precedence 50
for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s =
- (cic:/matita/dama/uniform/cauchy.con _ s).
+interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
(* Definition 2.15 *)
definition uniform_converge ≝
notation > "a 'uniform_converges' x" non associative with precedence 50
for @{'uniform_converge $a $x}.
interpretation "Uniform convergence" 'uniform_converge s u =
- (cic:/matita/dama/uniform/uniform_converge.con _ s u).
+ (uniform_converge _ s u).
(* Lemma 2.16 *)
lemma uniform_converge_is_cauchy :
cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
apply (Hn ? H1);
qed.
-
-(* Definition 2.17 *)
-definition mk_big_set ≝
- λP:CProp.λF:P→CProp.F.
-interpretation "explicit big set" 'explicitset t =
- (cic:/matita/dama/uniform/mk_big_set.con _ t).
-
-definition restrict_uniformity ≝
- λC:uniform_space.λX:C→Prop.
- {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.
-
-
projects / helm.git / blobdiff