]
qed.
-interpretation "Ordered uniform space segment" 'segment_set a =
+interpretation "Ordered uniform space segment" 'segset a =
(segment_ordered_uniform_space _ a).
(* Lemma 3.2 *)
lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀s:‡O.
∀x:{[s]}.
- ∀a:sequence (segment_ordered_uniform_space O s).
+ ∀a:sequence {[s]}.
(⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) →
a uniform_converges x.
intros 7; cases H1; cases H2; clear H2 H1;