notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
-interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
-interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
+interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l ?)).
+interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r ?)).
lemma h_segment_preserves_uparrow:
∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
-interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
-interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
+interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l ?)).
+interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r ?)).
(* Fact 2.18 *)
lemma segment_cauchy:
notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.
notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'downarrow_to_in_segment}.
-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 _)).
+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: