include "nat/le_arith.ma".
include "russell_support.ma".
+lemma hint1:
+ ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
+ → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set l u))).
+intros; assumption;
+qed.
+
+coercion hint1 nocomposites.
+
alias symbol "pi1" = "exT \fst".
-alias symbol "leq" = "natural 'less or equal to'".
+alias symbol "N" = "ordered set N".
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫;
fold normalize X; intros; cases H1;
-alias symbol "plus" = "natural plus".
-alias symbol "N" = "Uniform space N".
-alias symbol "and" = "logical and".
+alias symbol "N" = "Natural numbers".
letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j)));
(* s - aj <= max 0 (u - i) *)
letin m ≝ (hide ? (
rewrite > (H4 ?); [2: reflexivity]
apply le_to_le_to_eq;
[1: apply os_le_to_nat_le;
- apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));
+ apply (trans_increasing ? H ? ? (nat_le_to_os_le ?? H5));
|2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
rewrite < (H4 ?); [2: reflexivity] apply le_n;]
qed.
-alias symbol "pi1" = "exT \fst".
-alias symbol "leq" = "natural 'less or equal to'".
+lemma hint2:
+ ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
+ → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set l u))).
+intros; assumption;
+qed.
+
+coercion hint2 nocomposites.
+
alias symbol "N" = "ordered set N".
axiom nat_dedekind_sigma_complete_r:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing →
∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
+