include "supremum.ma".
-
(* Definition 2.13 *)
-alias symbol "square" = "bishop set square".
-alias symbol "pair" = "pair".
+alias symbol "pair" = "Pair construction".
alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
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〉.
+ λC:bishop_set.λU,V:C squareB → Prop.
+ λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd 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〉.
+ λ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).
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 @{ 'invert_appl $s $x}.
-notation > "'inv'" right associative with precedence 70
- for @{ 'invert_symbol }.
+ λ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).
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;
- 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));
- 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)
+ us_unifbase: (us_carr squareB → Prop) → CProp;
+ us_phi1: ∀U:us_carr squareB → Prop. us_unifbase U →
+ (λx:us_carr squareB.\fst x ≈ \snd x) ⊆ U;
+ us_phi2: ∀U,V:us_carr squareB → Prop. us_unifbase U → us_unifbase V →
+ ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
+ us_phi3: ∀U:us_carr squareB → Prop. us_unifbase U →
+ ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
+ us_phi4: ∀U:us_carr squareB → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
}.
(* Definition 2.14 *)
λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
-notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
+notation < "a \nbsp 'is_cauchy'" non associative with precedence 45
for @{'cauchy $a}.
-notation > "a 'is_cauchy'" non associative with precedence 50
+notation > "a 'is_cauchy'" non associative with precedence 45
for @{'cauchy $a}.
interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
λC:uniform_space.λa:sequence C.λu:C.
∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉.
-notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
+notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
for @{'uniform_converge $a $x}.
-notation > "a 'uniform_converges' x" non associative with precedence 50
+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).