λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
-interpretation "bs_of_ss" 'bsss x =
- (cic:/matita/dama/ordered_uniform/bs_of_ss.con _ _ _ x).
+interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
lemma segment_ordered_uniform_space:
∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
qed.
interpretation "Ordered uniform space segment" 'segment_set a b =
- (cic:/matita/dama/ordered_uniform/segment_ordered_uniform_space.con _ a b).
+ (segment_ordered_uniform_space _ a b).
(* Lemma 3.2 *)
alias symbol "pi1" = "sigma pi1".
-lemma foo:
+lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀l,u:O.
∀x:{[l,u]}.
∀a:sequence {[l,u]}.
apply (restrict ? l u ??? H4); apply (Hm ? H1);
qed.
+definition order_continuity ≝
+ λC:ordered_uniform_space.∀a:sequence C.∀x:C.
+ (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).