interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)).
interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)).
+alias symbol "dependent_pair" = "dependent pair".
(* Lemma 3.8 NON DUALIZZATO *)
lemma restrict_uniform_convergence_uparrow:
∀C:ordered_uniform_space.property_sigma C →
simplify; intros; cases (a i); assumption;
|2: intros;
lapply (uparrow_upperlocated a ≪x,h≫) as Ha1;
- [2: apply (segment_preserves_uparrow s); assumption;]
+ [2: apply (segment_preserves_uparrow s); assumption;]
lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2;
cases Ha2; clear Ha2;
cases (H1 a a); lapply (H5 H3 Ha1) as HaC;
lapply (segment_cauchy C s ? HaC) as Ha;
lapply (sigma_cauchy ? H ? x ? Ha); [left; assumption]
- apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)]
+ apply (restric_uniform_convergence C s ≪?,h≫ a Hletin)]
qed.
lemma hint_mah1:
- ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
+ ∀C. Type_OF_ordered_uniform_space__1 C → hos_carr (os_r C).
intros; assumption; qed.
coercion hint_mah1 nocomposites.