(* *)
(**************************************************************************)
-include "supremum.ma".
+include "dama/supremum.ma".
(* Definition 2.13 *)
alias symbol "pair" = "Pair construction".
λC:ordered_set.λU,V:C squareB → Prop.
λx:C squareB.∃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).
+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_bs_relation ≝
λC:bishop_set.λU:C squareB → Prop.
λx:C squareB. U 〈\snd x,\fst x〉.
notation > "\inv" with precedence 60 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).
+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".
for @{'cauchy $a}.
notation > "a 'is_cauchy'" non associative with precedence 45
for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
+interpretation "Cauchy sequence" 'cauchy s = (cauchy ? s).
(* Definition 2.15 *)
definition uniform_converge ≝
notation > "a 'uniform_converges' x" non associative with precedence 45
for @{'uniform_converge $a $x}.
interpretation "Uniform convergence" 'uniform_converge s u =
- (uniform_converge _ s u).
+ (uniform_converge ? s u).
(* Lemma 2.16 *)
lemma uniform_converge_is_cauchy :