+definition upper_bound ≝
+ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
+
+definition lower_bound ≝
+ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
+
+definition strong_sup ≝
+ λO:pordered_set.λs:sequence O.λx.
+ upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
+
+definition strong_inf ≝
+ λO:pordered_set.λs:sequence O.λx.
+ lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n).
+
+definition weak_sup ≝
+ λO:pordered_set.λs:sequence O.λx.
+ upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
+
+definition weak_inf ≝
+ λO:pordered_set.λs:sequence O.λx.
+ lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x).
+
+lemma strong_sup_is_weak:
+ ∀O:pordered_set.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
+intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
+intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
+qed.
+
+lemma strong_inf_is_weak:
+ ∀O:pordered_set.∀s:sequence O.∀x:O.strong_inf ? s x → weak_inf ? s x.
+intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
+intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
+qed.
+
+
+
+definition increasing ≝
+ λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
+
+definition decreasing ≝
+ λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
+
+
+(*