1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sandwich_corollary.ma".
19 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
20 increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
23 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
24 decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
28 ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → (* BUG again the wrong coercion is chosen *)
29 ∀x,y:apart_of_metric_space ? ml.supremum ?? xn x → supremum ?? xn y → x ≈ y.
30 intros (R ml xn Hxn x y Sx Sy);
31 elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
32 apply (tends_uniq ?? xn ?? Hx Hy);