-metric_lattice.ma excess.ma lattice.ma metric_space.ma
+metric_lattice.ma lattice.ma metric_space.ma
metric_space.ma ordered_divisible_group.ma
-sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma sequence.ma
+sandwich.ma nat/orders.ma nat/plus.ma tend.ma
premetric_lattice.ma lattice.ma metric_space.ma
ordered_group.ma group.ma
divisible_group.ma group.ma nat/orders.ma
ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma
-sequence.ma excess.ma nat/orders.ma ordered_group.ma
+sequence.ma excess.ma
constructive_connectives.ma logic/connectives.ma
lattice.TF.ma excess.ma lattice.ma nat/nat.ma
group.ma excess.ma
prevalued_lattice.ma ordered_group.ma
excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
-sandwich_corollary.ma metric_lattice.ma sandwich.ma
+sandwich_corollary.ma sandwich.ma
Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
+limit.ma excess.ma infsup.ma tend.ma
lattice.ma excess.ma
+tend.ma metric_lattice.ma nat/orders.ma sequence.ma
constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
-infsup.ma sandwich_corollary.ma
+infsup.ma excess.ma sequence.ma
constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma
classical_pointwise/topology.ma classical_pointwise/sets.ma
classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma
record excess_ : Type ≝ {
exc_exc:> excess_base;
- exc_ap: apartness;
- exc_with: ap_carr exc_ap = exc_carr exc_exc
+ exc_ap_: apartness;
+ exc_with: ap_carr exc_ap_ = exc_carr exc_exc
}.
-definition apart_of_excess_: excess_ → apartness.
+definition exc_ap: excess_ → apartness.
intro E; apply (mk_apartness E); unfold Type_OF_excess_;
cases (exc_with E); simplify;
-[apply (ap_apart (exc_ap E));
+[apply (ap_apart (exc_ap_ E));
|apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive]
qed.
-coercion cic:/matita/excess/apart_of_excess_.con.
+coercion cic:/matita/excess/exc_ap.con.
record excess : Type ≝ {
excess_carr:> excess_;
[ apply (λx,y:E.y≰x);|apply exc_coreflexive;
| unfold cotransitive; simplify; intros (x y z H);
cases (exc_cotransitive E ??z H);[right|left]assumption]
- |2: apply (exc_ap E);
+ |2: apply (exc_ap_ E);
|3: apply (exc_with E);]
|2: simplify; intros (y x H); fold simplify (y#x) in H;
apply ap2exc; apply ap_symmetric; apply H;
(* *)
(**************************************************************************)
-include "sandwich_corollary.ma".
+include "sequence.ma".
-(* 3.19 *)
-definition supremum ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
+definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-definition infimum ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
-
-(* 3.20 *)
-lemma supremum_uniq:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn →
- ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
-intros (R ml xn Hxn x y Sx Sy);
-elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
-apply (tends_uniq ?? xn ?? Hx Hy);
-qed.
+definition strong_sup ≝
+ λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
-definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
- λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
-
-definition ank ≝
- λR.λml:mlattice R.λxn:sequence ml.λk:nat.
- let rec ank_aux (i : nat) ≝
- match i with
- [ O ⇒ (shift ?? xn k) O
- | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
- in ank_aux.
-
-notation < "'a'\sup k" non associative with precedence 50 for
- @{ 'ank $x $k }.
-
-interpretation "ank" 'ank x k =
- (cic:/matita/infsup/ank.con _ _ x k).
+definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
-notation < "'a'(k \atop n)" non associative with precedence 50 for
- @{ 'ank2 $x $k $n }.
-
-interpretation "ank2" 'ank2 x k n =
- (cic:/matita/infsup/ank.con _ _ x k n).
-
-definition bnk ≝
- λR.λml:mlattice R.λxn:sequence ml.λk:nat.
- let rec bnk_aux (i : nat) ≝
- match i with
- [ O ⇒ (shift ?? xn k) O
- | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
- in bnk_aux.
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}.
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $s $x}.
+notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $s}.
+notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $s $x}.
+notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $s $x}.
-notation < "'b'\sup k" non associative with precedence 50 for
- @{ 'bnk $x $k }.
-
-interpretation "bnk" 'bnk x k =
- (cic:/matita/infsup/bnk.con _ _ x k).
+notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}.
+notation > "x 'is_lower_bound' s" non associative with precedence 50 for @{'lower_bound $s $x}.
+notation > "s 'is_increasing'" non associative with precedence 50 for @{'increasing $s}.
+notation > "s 'is_decreasing'" non associative with precedence 50 for @{'decreasing $s}.
+notation > "x 'is_strong_sup' s" non associative with precedence 50 for @{'strong_sup $s $x}.
+notation > "x 'is_strong_inf' s" non associative with precedence 50 for @{'strong_inf $s $x}.
-notation < "('b' \sup k) \sub n" non associative with precedence 50 for
- @{ 'bnk2 $x $k $n }.
-
-interpretation "bnk2" 'bnk2 x k n =
- (cic:/matita/infsup/bnk.con _ _ x k n).
-
-lemma ank_decreasing:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
-intros (R ml xn k); unfold; intro n; simplify; apply lem;
-qed.
+interpretation "Excess upper bound" 'upper_bound s x = (cic:/matita/infsup/upper_bound.con _ s x).
+interpretation "Excess lower bound" 'lower_bound s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con _) s x).
+interpretation "Excess increasing" 'increasing s = (cic:/matita/infsup/increasing.con _ s).
+interpretation "Excess decreasing" 'decreasing s = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con _) s).
+interpretation "Excess strong sup" 'strong_sup s x = (cic:/matita/infsup/strong_sup.con _ s x).
+interpretation "Excess strong inf" 'strong_inf s x = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con _) s x).
-(* 3.26 *)
-lemma ankS:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
- ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
-intros (R ml xn k n); elim n; simplify; [apply meet_comm]
-simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
-apply (Eq≈ ? (meet_assoc ????));
-apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
-apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply meet_comm;
-qed.
+definition seq_dual_exc_hint: ∀E.sequence E → sequence (dual_exc E) ≝ λE.λx:sequence E.x.
+definition seq_dual_exc_hint1: ∀E.sequence (dual_exc E) → sequence E ≝ λE.λx:sequence (dual_exc E).x.
-lemma bnkS:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
- ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n).
-intros (R ml xn k n); elim n; simplify; [apply join_comm]
-simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H;
-apply (Eq≈ ? (join_assoc ????));
-apply (Eq≈ ?? (eq_sym ??? (join_assoc ????)));
-apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply join_comm;
-qed.
-
-lemma le_asnk_ansk:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
- (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
-intros (R ml xn k n);
-apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
-qed.
-
-lemma le_bnsk_bsnk:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
- (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)).
-intros (R ml xn k n);
-apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????));
-apply (Le≫ ? (join_comm ???));
-apply lej;
-qed.
-
-
-(* 3.27 *)
-lemma inf_increasing:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.
- ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) →
- increasing ml alpha.
-intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold;
-intro r;
-elim (H r) (H1r H2r);
-elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
-intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
-lapply (H1r (S w)) as Hsw; clear H1r;
-lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;
-cases (H Hw);
-qed.
-
-lemma sup_decreasing:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.
- ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) →
- decreasing ml alpha.
-intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
-intro r;
-elim (H r) (H1r H2r);
-elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
-intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
-lapply (H1r (S w)) as Hsw; clear H1r;
-lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H;
-cases (H Hw);
-qed.
-
-(* 3.28 *)
-definition liminf ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- ∃alpha:sequence ml.
- (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
-
-definition limsup ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- ∃alpha:sequence ml.
- (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
-
-(* 3.29 *)
-alias symbol "and" = "constructive and".
-definition lim ≝
- λR.λml:mlattice R.λxn:sequence ml.λx:ml.
- (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
-
-(* 3.30 *)
-lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
- lim ?? xn x → xn ⇝ x.
-intros (R ml xn x Hl);
-unfold in Hl; unfold limsup in Hl; unfold liminf in Hl;
-(* decompose; *)
-elim Hl (low Hl_); clear Hl;
-elim Hl_ (up Hl); clear Hl_;
-elim Hl (Hl_ E1); clear Hl;
-elim Hl_ (Hl E2); clear Hl_;
-elim Hl (H1 H2); clear Hl;
-elim H1 (alpha Halpha); clear H1;
-elim H2 (beta Hbeta); clear H2;
-apply (sandwich ?? alpha beta);
-[1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
- lapply (sup_increasing ????? Ha6) as Ha7;
-
- unfold strong_sup in Halpha Hbeta;
- unfold strong_inf in Halpha Hbeta;
- unfold lower_bound in Halpha Hbeta;
- unfold upper_bound in Halpha Hbeta;
- elim (Halpha m) (Ha5 Ha6); clear Halpha;
- elim Ha5 (Ha1 Ha2); clear Ha5;
- elim Ha6 (Ha3 Ha4); clear Ha6;
- split;
- [1: intro H; elim (Ha2 ? H) (w H1);
- elim (Ha4 ? H1);
-
-
-
-
\ No newline at end of file
+coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites.
+coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites.
record semi_lattice : Type ≝ {
sl_exc:> excess;
- meet: sl_exc → sl_exc → sl_exc;
- meet_refl: ∀x.meet x x ≈ x;
- meet_comm: ∀x,y. meet x y ≈ meet y x;
- meet_assoc: ∀x,y,z. meet x (meet y z) ≈ meet (meet x y) z;
- strong_extm: ∀x.strong_ext ? (meet x);
- le_to_eqm: ∀x,y.x ≤ y → x ≈ meet x y;
- lem: ∀x,y.(meet x y) ≤ y
+ sl_meet: sl_exc → sl_exc → sl_exc;
+ sl_meet_refl: ∀x.sl_meet x x ≈ x;
+ sl_meet_comm: ∀x,y. sl_meet x y ≈ sl_meet y x;
+ sl_meet_assoc: ∀x,y,z. sl_meet x (sl_meet y z) ≈ sl_meet (sl_meet x y) z;
+ sl_strong_extm: ∀x.strong_ext ? (sl_meet x);
+ sl_le_to_eqm: ∀x,y.x ≤ y → x ≈ sl_meet x y;
+ sl_lem: ∀x,y.(sl_meet x y) ≤ y
}.
-interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/meet.con _ a b).
+interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
-lemma feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
+lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
-intro H1; apply H; clear H; apply (strong_extm ???? H1);
+intro H1; apply H; clear H; apply (sl_strong_extm ???? H1);
qed.
-lemma feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
+lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
intros (l a b c H);
-apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
-apply feq_ml; assumption;
+apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???));
+apply sl_feq_ml; assumption;
qed.
apply (mk_semi_lattice (dual_exc l));
unfold excess_OF_lattice_;
cases (latt_with l); simplify;
-[apply meet|apply meet_refl|apply meet_comm|apply meet_assoc|
-apply strong_extm| apply le_to_eqm|apply lem]
+[apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc|
+apply sl_strong_extm| apply sl_le_to_eqm|apply sl_lem]
qed.
coercion cic:/matita/lattice/latt_jcarr.con.
interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
interpretation "Lattice join" 'or a b =
- (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
+ (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
record lattice : Type ≝ {
latt_carr:> lattice_;
notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
notation "'lej'" non associative with precedence 50 for @{'lej}.
-interpretation "Lattice meet" 'meet = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice lem" 'lem = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice join" 'join = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice lej" 'lej = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
-interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
-interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
+
+interpretation "Lattive meet le" 'leq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
+
+interpretation "Lattive join le (aka ge)" 'geq a b =
+ (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
+
+(* these coercions help unification, handmaking a bit of conversion
+ over an open term
+*)
+lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
+intros(l a b H); apply H;
+qed.
+
+lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
+intros(l a b H); apply H;
+qed.
+
+coercion cic:/matita/lattice/le_to_ge.con nocomposites.
+coercion cic:/matita/lattice/ge_to_le.con nocomposites.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "infsup.ma".
+
+(* 3.28 *)
+definition limsup ≝
+ λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E.
+ (∀k.(alpha k) is_strong_sup xn) ∧ x is_strong_inf alpha.
+
+notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $s $x}.
+notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $s $x}.
+notation > "x 'is_limsup' s" non associative with precedence 50 for @{'limsup $s $x}.
+notation > "x 'is_liminf' s" non associative with precedence 50 for @{'liminf $s $x}.
+
+interpretation "Excess limsup" 'limsup s x = (cic:/matita/limit/limsup.con _ s x).
+interpretation "Excess liminf" 'liminf s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con _) s x).
+
+(* 3.29 *)
+definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn ∧ x is_liminf xn.
+
+notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $s $x}.
+notation > "x 'is_lim' s" non associative with precedence 50 for @{'lim $s $x}.
+interpretation "Excess lim" 'lim s x = (cic:/matita/limit/lim.con _ s x).
+
+lemma sup_decreasing:
+ ∀E:excess.∀xn:sequence E.
+ ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn) →
+ alpha is_decreasing.
+intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
+intro r;
+elim (H r) (H1r H2r);
+elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
+intro e; cases (H2sr (alpha r) e) (w Hw); clear e H2sr;
+cases (H1r w Hw);
+qed.
+
+include "tend.ma".
+
+(* 3.30 *)
+lemma lim_tends:
+ ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
+ x is_lim xn → xn ⇝ x.
+intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl;
+
record mlattice_ (R : todgroup) : Type ≝ {
ml_mspace_: metric_space R;
ml_lattice:> lattice;
- ml_with_: ms_carr ? ml_mspace_ = apart_of_excess (pl_carr ml_lattice)
+ ml_with: ms_carr ? ml_mspace_ = Type_OF_lattice ml_lattice
}.
lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
-intros (R ml); apply (mk_metric_space R (apart_of_excess ml));
-unfold apartness_OF_mlattice_;
-[rewrite < (ml_with_ ? ml); apply (metric ? (ml_mspace_ ? ml))]
-cases (ml_with_ ? ml); simplify;
-[apply (mpositive ? (ml_mspace_ ? ml));|apply (mreflexive ? (ml_mspace_ ? ml));
-|apply (msymmetric ? (ml_mspace_ ? ml));|apply (mtineq ? (ml_mspace_ ? ml))]
+intros (R ml); apply (mk_metric_space R (Type_OF_mlattice_ ? ml));
+unfold Type_OF_mlattice_; cases (ml_with ? ml); simplify;
+[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml));
+|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml));
+|apply (mtineq ? (ml_mspace_ ? ml))]
qed.
coercion cic:/matita/metric_lattice/ml_mspace.con.
alias symbol "plus" = "Abelian group plus".
+alias symbol "leq" = "ordered sets less or equal than".
record mlattice (R : todgroup) : Type ≝ {
ml_carr :> mlattice_ R;
ml_prop1: ∀a,b:ml_carr. 0 < δ a b → a # b;
- ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ δ b c
+ ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ (δ b c)
}.
lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b.
intros; apply (eq_trans ???? (msymmetric ??y x));
apply (eq_trans ????? (msymmetric ??z y)); apply meq_l; assumption;
qed.
-
lemma dap_to_lt: ∀R.∀ml:mlattice R.∀x,y:ml. δ x y # 0 → 0 < δ x y.
intros; split [apply mpositive] apply ap_symmetric; assumption;
apply ap_symmetric; assumption;
qed.
-interpretation "Lattive meet le" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
-
-interpretation "Lattive join le (aka ge)" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
-
-lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
-intros(l a b H); apply H;
-qed.
-
-lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
-intros(l a b H); apply H;
-qed.
-
-lemma eq_to_eq:∀l:lattice.∀a,b:l.
- (eq (apart_of_excess (pl_carr (latt_jcarr l))) a b) →
- (eq (apart_of_excess (pl_carr (latt_mcarr l))) a b).
-intros 3; unfold eq; unfold apartness_OF_lattice;
-unfold apartness_OF_lattice_1; unfold latt_jcarr; simplify;
-unfold dual_exc; simplify; intros 2 (H H1); apply H;
-cases H1;[right|left]assumption;
-qed.
-
-coercion cic:/matita/metric_lattice/eq_to_eq.con nocomposites.
-
(* 3.11 *)
lemma le_mtri:
∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
lapply (le_to_eqm ?? Lxy) as Dxm; lapply (le_to_eqm ?? Lyz) as Dym;
-lapply (le_to_eqj ?? (le_to_ge ??? Lxy)) as Dxj; lapply (le_to_eqj ?? (le_to_ge ??? Lyz)) as Dyj; clear Lxy Lyz;
+lapply (le_to_eqj ?? Lxy) as Dxj; lapply (le_to_eqj ?? Lyz) as Dyj; clear Lxy Lyz;
apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) z));[
- apply feq_plusl; apply meq_l; clear Dyj Dxm Dym;
- unfold apartness_OF_mlattice1;
- exact (eq_to_eq ??? Dxj);]
+ apply feq_plusl; apply meq_l; clear Dyj Dxm Dym; assumption]
apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) (z∨y))); [
apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (y∨x) ? Dyj));]
apply (Eq≈ ? (plus_comm ???));
apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)));[
- apply feq_plusr;
- apply meq_r;
- apply (join_comm y z);]
+ apply feq_plusr; apply meq_r; apply (join_comm ??);]
apply feq_plusl;
-apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm x y)));
+apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ??)));
apply eq_reflexive;
qed.
(* *)
(**************************************************************************)
-
-
include "ordered_divisible_group.ma".
-record metric_space (R : todgroup) : Type ≝ {
+record metric_space (R: todgroup) : Type ≝ {
ms_carr :> Type;
metric: ms_carr → ms_carr → R;
mpositive: ∀a,b:ms_carr. 0 ≤ metric a b;
notation "\delta" non associative with precedence 80 for @{ 'delta }.
interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
-definition apart_metric:=
- λR.λms:metric_space R.λa,b:ms.0 < δ a b.
-
-lemma apart_of_metric_space: ∀R:todgroup.metric_space R → apartness.
-intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold;
-[1: intros 2 (x H); cases H (H1 H2);
- lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2);
+lemma apart_of_metric_space: ∀R.metric_space R → apartness.
+intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
+[1: intros 2 (x H); cases H (H1 H2); clear H;
+ lapply (Ap≫ ? (eq_sym ??? (mreflexive ??x)) H2);
apply (ap_coreflexive R 0); assumption;
|2: intros (x y H); cases H; split;
- [1: apply (le_rewr ???? (msymmetric ????)); assumption
- |2: apply (ap_rewr ???? (msymmetric ????)); assumption]
-|3: simplify; intros (x y z H); cases H (LExy Axy);
- lapply (mtineq ?? x y z) as H1; whd in Axy; cases Axy (H2 H2); [cases (LExy H2)]
+ [1: apply (Le≫ ? (msymmetric ????)); assumption
+ |2: apply (Ap≫ ? (msymmetric ????)); assumption]
+|3: simplify; intros (x y z H); elim H (LExy Axy);
+ lapply (mtineq ?? x y z) as H1; elim (ap2exc ??? Axy) (H2 H2); [cases (LExy H2)]
clear LExy; lapply (lt_le_transitive ???? H H1) as LT0;
apply (lt0plus_orlt ????? LT0); apply mpositive;]
qed.
-(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
-
lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
intros 2 (R m); cases m 0; simplify; intros; assumption; qed.
record pogroup_ : Type ≝ {
og_abelian_group_: abelian_group;
og_excess:> excess;
- og_with: carr og_abelian_group_ = apart_of_excess og_excess
+ og_with: carr og_abelian_group_ = exc_ap og_excess
}.
lemma og_abelian_group: pogroup_ → abelian_group.
-intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)]
-[apply (plus (og_abelian_group_ G));|apply zero;|apply opp]
-unfold apartness_OF_pogroup_; cases (og_with G); simplify;
-[apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
+intro G; apply (mk_abelian_group G); unfold apartness_OF_pogroup_;
+cases (og_with G); simplify;
+[apply (plus (og_abelian_group_ G));|apply zero;|apply opp
+|apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
qed.
coercion cic:/matita/ordered_group/og_abelian_group.con.
intros 3 (x y z); rewrite > sym_plus; apply ltwl;
qed.
-include "sequence.ma".
-include "metric_lattice.ma".
-
-definition d2s ≝
- λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
-
-notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
-
-interpretation "tends to" 'tends s x =
- (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
+include "tend.ma".
+alias symbol "leq" = "ordered sets less or equal than".
+alias symbol "and" = "constructive and".
theorem sandwich:
let ugo ≝ excess_OF_lattice1 in
∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
- (∀n. (le (excess_OF_lattice1 ml) (xn n) (an n)) ∧
- (le (excess_OF_lattice1 ?) (bn n) (xn n))) → True.
+ (∀n. (xn n ≤ an n) ∧ (bn n ≤ xn n)) →
an ⇝ x → bn ⇝ x → xn ⇝ x.
intros (R ml an bn xn x H Ha Hb);
unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
include "sandwich.ma".
-include "metric_lattice.ma".
-
(* 3.17 *)
lemma tends_uniq:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.
- ∀x,y:ml.
- (* BUG: it inserts a compesoed coercion instead of an hand made one,
- what to do? prefer the human made one or allow to kill a coercion?
- *)
+ ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x,y:ml.
xn ⇝ x → xn ⇝ y → δ x y ≈ 0.
intros (R ml xn x y H1 H2); unfold tends0 in H1 H2; unfold d2s in H1 H2;
intro Axy; lapply (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0;
(* *)
(**************************************************************************)
-
-
include "excess.ma".
definition sequence := λO:excess.nat → O.
-definition fun_of_sequence: ∀O:excess.sequence O → nat → O.
-intros; apply s; assumption;
-qed.
+definition fun_of_sequence: ∀O:excess.sequence O → nat → O ≝ λO.λx:sequence O.x.
coercion cic:/matita/sequence/fun_of_sequence.con 1.
-
-definition upper_bound ≝
- λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-
-definition lower_bound ≝
- λO:excess.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
-
-definition strong_sup ≝
- λO:excess.λs:sequence O.λx.
- upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
-
-definition strong_inf ≝
- λO:excess.λs:sequence O.λx.
- lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n).
-
-definition weak_sup ≝
- λO:excess.λs:sequence O.λx.
- upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
-
-definition weak_inf ≝
- λO:excess.λs:sequence O.λx.
- lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x).
-
-lemma strong_sup_is_weak:
- ∀O:excess.∀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:excess.∀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.
-
-include "ordered_group.ma".
-include "nat/orders.ma".
-
-definition tends0 ≝
- λO:pogroup.λs:sequence O.
- ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
-
-definition increasing ≝
- λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
-
-definition decreasing ≝
- λO:excess.λa:sequence O.∀n:nat.a (S n) ≤ a n.
-
-
-
-
-(*
-
-definition is_upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-definition is_lower_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
-
-record is_sup (O:excess) (a:sequence O) (u:O) : Prop ≝
- { sup_upper_bound: is_upper_bound O a u;
- sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
- }.
-
-record is_inf (O:excess) (a:sequence O) (u:O) : Prop ≝
- { inf_lower_bound: is_lower_bound O a u;
- inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
- }.
-
-record is_bounded_below (O:excess) (a:sequence O) : Type ≝
- { ib_lower_bound: O;
- ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
- }.
-
-record is_bounded_above (O:excess) (a:sequence O) : Type ≝
- { ib_upper_bound: O;
- ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
- }.
-
-record is_bounded (O:excess) (a:sequence O) : Type ≝
- { ib_bounded_below:> is_bounded_below ? a;
- ib_bounded_above:> is_bounded_above ? a
- }.
-
-record bounded_below_sequence (O:excess) : Type ≝
- { bbs_seq:> sequence O;
- bbs_is_bounded_below:> is_bounded_below ? bbs_seq
- }.
-
-record bounded_above_sequence (O:excess) : Type ≝
- { bas_seq:> sequence O;
- bas_is_bounded_above:> is_bounded_above ? bas_seq
- }.
-
-record bounded_sequence (O:excess) : Type ≝
- { bs_seq:> sequence O;
- bs_is_bounded_below: is_bounded_below ? bs_seq;
- bs_is_bounded_above: is_bounded_above ? bs_seq
- }.
-
-definition bounded_below_sequence_of_bounded_sequence ≝
- λO:excess.λb:bounded_sequence O.
- mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
-
-coercion cic:/matita/sequence/bounded_below_sequence_of_bounded_sequence.con.
-
-definition bounded_above_sequence_of_bounded_sequence ≝
- λO:excess.λb:bounded_sequence O.
- mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
-
-coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
-
-definition lower_bound ≝
- λO:excess.λb:bounded_below_sequence O.
- ib_lower_bound ? b (bbs_is_bounded_below ? b).
-
-lemma lower_bound_is_lower_bound:
- ∀O:excess.∀b:bounded_below_sequence O.
- is_lower_bound ? b (lower_bound ? b).
-intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
-qed.
-
-definition upper_bound ≝
- λO:excess.λb:bounded_above_sequence O.
- ib_upper_bound ? b (bas_is_bounded_above ? b).
-
-lemma upper_bound_is_upper_bound:
- ∀O:excess.∀b:bounded_above_sequence O.
- is_upper_bound ? b (upper_bound ? b).
-intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
-qed.
-
-definition reverse_excess: excess → excess.
-intros (E); apply (mk_excess E); [apply (λx,y.exc_relation E y x)]
-cases E (T f cRf cTf); simplify;
-[1: unfold Not; intros (x H); apply (cRf x); assumption
-|2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
-qed.
-
-definition reverse_excess: excess → excess.
-intros (p); apply (mk_excess (reverse_excess p));
-generalize in match (reverse_excess p); intros (E);
-apply mk_is_porder_relation;
-[apply le_reflexive|apply le_transitive|apply le_antisymmetric]
-qed.
-
-lemma is_lower_bound_reverse_is_upper_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
- is_lower_bound O a l → is_upper_bound (reverse_excess O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess;
-unfold reverse_excess; simplify; fold unfold le (le ? l (a n)); apply H;
-qed.
-
-lemma is_upper_bound_reverse_is_lower_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
- is_upper_bound O a l → is_lower_bound (reverse_excess O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess;
-unfold reverse_excess; simplify; fold unfold le (le ? (a n) l); apply H;
-qed.
-
-lemma reverse_is_lower_bound_is_upper_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
- is_lower_bound (reverse_excess O) a l → is_upper_bound O a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess in H;
-unfold reverse_excess in H; simplify in H; apply H;
-qed.
-
-lemma reverse_is_upper_bound_is_lower_bound:
- ∀O:excess.∀a:sequence O.∀l:O.
- is_upper_bound (reverse_excess O) a l → is_lower_bound O a l.
-intros (O a l H); unfold; intros (n); unfold reverse_excess in H;
-unfold reverse_excess in H; simplify in H; apply H;
-qed.
-
-lemma is_inf_to_reverse_is_sup:
- ∀O:excess.∀a:bounded_below_sequence O.∀l:O.
- is_inf O a l → is_sup (reverse_excess O) a l.
-intros (O a l H); apply (mk_is_sup (reverse_excess O));
-[1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
-|2: unfold reverse_excess; simplify; unfold reverse_excess; simplify;
- intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
-qed.
-
-lemma is_sup_to_reverse_is_inf:
- ∀O:excess.∀a:bounded_above_sequence O.∀l:O.
- is_sup O a l → is_inf (reverse_excess O) a l.
-intros (O a l H); apply (mk_is_inf (reverse_excess O));
-[1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
-|2: unfold reverse_excess; simplify; unfold reverse_excess; simplify;
- intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
-qed.
-
-lemma reverse_is_sup_to_is_inf:
- ∀O:excess.∀a:bounded_above_sequence O.∀l:O.
- is_sup (reverse_excess O) a l → is_inf O a l.
-intros (O a l H); apply mk_is_inf;
-[1: apply reverse_is_upper_bound_is_lower_bound;
- apply (sup_upper_bound (reverse_excess O)); assumption
-|2: intros (v H1); apply (sup_least_upper_bound (reverse_excess O) a l H v);
- apply is_lower_bound_reverse_is_upper_bound; assumption;]
-qed.
-
-lemma reverse_is_inf_to_is_sup:
- ∀O:excess.∀a:bounded_above_sequence O.∀l:O.
- is_inf (reverse_excess O) a l → is_sup O a l.
-intros (O a l H); apply mk_is_sup;
-[1: apply reverse_is_lower_bound_is_upper_bound;
- apply (inf_lower_bound (reverse_excess O)); assumption
-|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_excess O) a l H v);
- apply is_upper_bound_reverse_is_lower_bound; assumption;]
-qed.
-
-*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "sequence.ma".
+include "metric_lattice.ma". (* we should probably use something weaker *)
+include "nat/orders.ma".
+
+definition tends0 ≝
+ λO:pogroup.λs:sequence O.∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
+
+definition d2s ≝
+ λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
+
+notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
+interpretation "tends to" 'tends s x =
+ (cic:/matita/tend/tends0.con _ (cic:/matita/tend/d2s.con _ _ s x)).
+
projects / helm.git / commitdiff