include "nat/le_arith.ma".
include "russell_support.ma".
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
alias symbol "leq" = "natural 'less or equal to'".
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〉);
+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 "nat" = "Uniform space N".
+alias symbol "N" = "Uniform space N".
alias symbol "and" = "logical and".
letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j)));
(* s - aj <= max 0 (u - i) *)
rewrite < (H4 ?); [2: reflexivity] apply le_n;]
qed.
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
alias symbol "leq" = "natural 'less or equal to'".
-alias symbol "nat" = "ordered set N".
+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).