notation > "x 'is_infimum' s" non associative with precedence 45
for @{'infimum $s $x}.
-interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l _) s x).
-interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r _) s x).
+interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l ?) s x).
+interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r ?) s x).
-interpretation "Ordered set increasing" 'increasing s = (increasing (os_l _) s).
-interpretation "Ordered set decreasing" 'decreasing s = (increasing (os_r _) s).
+interpretation "Ordered set increasing" 'increasing s = (increasing (os_l ?) s).
+interpretation "Ordered set decreasing" 'decreasing s = (increasing (os_r ?) s).
-interpretation "Ordered set strong sup" 'supremum s x = (supremum (os_l _) s x).
-interpretation "Ordered set strong inf" 'infimum s x = (supremum (os_r _) s x).
+interpretation "Ordered set strong sup" 'supremum s x = (supremum (os_l ?) s x).
+interpretation "Ordered set strong inf" 'infimum s x = (supremum (os_r ?) s x).
(* Fact 2.5 *)
lemma h_supremum_is_upper_bound:
notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
-interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
-interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
+interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l ?)).
+interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r ?)).
(* Lemma 2.6 *)
definition strictly_increasing ≝
notation > "s 'is_strictly_increasing'" non associative with precedence 45
for @{'strictly_increasing $s}.
interpretation "Ordered set strict increasing" 'strictly_increasing s =
- (strictly_increasing (os_l _) s).
+ (strictly_increasing (os_l ?) s).
notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
notation > "s 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
- (strictly_increasing (os_r _) s).
+ (strictly_increasing (os_r ?) s).
definition uparrow ≝
λC:half_ordered_set.λs:sequence C.λu:C.
increasing ? s ∧ supremum ? s u.
-interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
-interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
+interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l ?) s u).
+interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r ?) s u).
lemma h_trans_increasing:
∀C:half_ordered_set.∀a:sequence C.increasing ? a →
notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
-interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
-interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
+interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l ?)).
+interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r ?)).
lemma hint_nat :
Type_OF_ordered_set nat_ordered_set →
notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
-interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
-interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
+interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l ?)).
+interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r ?)).
alias symbol "exists" = "CProp exists".
lemma nat_strictly_increasing_reaches:
notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
-interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
-interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
+interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l ?)).
+interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r ?)).
(* Definition 2.7 *)
definition order_converge ≝
for @{'order_converge $a $x}.
notation > "a 'order_converges' x" non associative with precedence 45
for @{'order_converge $a $x}.
-interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
+interpretation "Order convergence" 'order_converge s u = (order_converge ? s u).
(* Definition 2.8 *)
record segment (O : Type) : Type ≝ {
seg_u_ : O
}.
-notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation > "𝕦_ term 90 s" non associative with precedence 90 for @{'upp $s}.
notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}.
-notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
+notation > "𝕝_ term 90 s" non associative with precedence 90 for @{'low $s}.
notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}.
definition seg_u ≝
λO:half_ordered_set.λs:segment O.
wloss O ?? (λl,u.l) (seg_l_ ? s) (seg_u_ ? s).
-interpretation "uppper" 'upp s = (seg_u (os_l _) s).
-interpretation "lower" 'low s = (seg_l (os_l _) s).
-interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
-interpretation "lower dual" 'low s = (seg_u (os_r _) s).
+interpretation "uppper" 'upp s = (seg_u (os_l ?) s).
+interpretation "lower" 'low s = (seg_l (os_l ?) s).
+interpretation "uppper dual" 'upp s = (seg_l (os_r ?) s).
+interpretation "lower dual" 'low s = (seg_u (os_r ?) s).
definition in_segment ≝
λO:half_ordered_set.λs:segment O.λx:O.
notation "‡O" non associative with precedence 90 for @{'segment $O}.
interpretation "Ordered set sergment" 'segment x = (segment x).
-interpretation "Ordered set sergment in" 'mem x s = (in_segment _ s x).
+interpretation "Ordered set sergment in" 'mem x s = (in_segment ? s x).
definition segment_ordered_set_carr ≝
λO:half_ordered_set.λs:‡O.∃x.x ∈ s.
qed.
notation "{[ term 19 s ]}" non associative with precedence 90 for @{'segset $s}.
-interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s).
+interpretation "Ordered set segment" 'segset s = (segment_ordered_set ? s).
(* test :
∀O:ordered_set.∀s: segment (os_l O).∀x:O.
notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
-interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
-interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
+interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l ?)).
+interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r ?)).
(*
test segment_preserves_infimum2:
notation > "s 'is_upper_located'" non associative with precedence 45
for @{'upper_located $s}.
interpretation "Ordered set upper locatedness" 'upper_located s =
- (upper_located (os_l _) s).
+ (upper_located (os_l ?) s).
notation < "s \nbsp 'is_lower_located'" non associative with precedence 45
for @{'lower_located $s}.
notation > "s 'is_lower_located'" non associative with precedence 45
for @{'lower_located $s}.
interpretation "Ordered set lower locatedness" 'lower_located s =
- (upper_located (os_r _) s).
+ (upper_located (os_r ?) s).
(* Lemma 2.12 *)
lemma h_uparrow_upperlocated:
notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
-interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
-interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).
+interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l ?)).
+interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r ?)).