(* *)
(**************************************************************************)
-include "uniform.ma".
+include "dama/uniform.ma".
record ordered_uniform_space_ : Type ≝ {
ous_os:> ordered_set;
λC:ordered_set.λU:C squareO → Prop.
λx:C squareO. U 〈\snd x,\fst x〉.
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+interpretation "relation invertion" 'invert a = (invert_os_relation ? a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation ?).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation ? a x).
lemma hint_segment: ∀O.
segment (Type_of_ordered_set O) →
change in H1:(? ? ? %) with (\fst b);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
- apply rule H1;
+ apply rule (x2sx_ ? s ?? H1);
| right; change in H1:(? ? % ?) with (\fst b);
change in H1:(? ? ? %) with (\fst a);
change in a with (hos_carr (half_segment_ordered_set ? s));
change in b with (hos_carr (half_segment_ordered_set ? s));
- apply rule H1;]
+ apply rule (x2sx_ ? s ?? H1);]
qed.
qed.
interpretation "Ordered uniform space segment" 'segset a =
- (segment_ordered_uniform_space _ a).
+ (segment_ordered_uniform_space ? a).
(* Lemma 3.2 *)
alias symbol "pi1" = "exT \fst".