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).
+interpretation "Bishop subset" 'subset a b = (subset _ 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).
+interpretation "explicit set" 'explicitset t = (mk_set _ 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).
+interpretation "bishop set square" 'square x = (square_bishop_set x).
+interpretation "bishop set square" 'square2 x = (square_bishop_set x).
alias symbol "exists" = "exists".
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).
+interpretation "relations composition" 'compose a b = (compose_relations _ 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).
+ (compose_relations _ a b x).
definition invert_relation ≝
λC:bishop_set.λU:C square → Prop.
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).
+interpretation "relation invertion" 'invert a = (invert_relation _ a).
+interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
alias symbol "exists" = "CProp exists".
alias symbol "and" (instance 18) = "constructive and".
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 :
(* 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).
+interpretation "explicit big set" 'explicitset t = (mk_big_set _ t).
definition restrict_uniformity ≝
λC:uniform_space.λX:C→Prop.