From 87ed0c3e2ccd74f21f81c2cc9ed2945109bf0a9a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Dec 2007 10:16:17 +0000 Subject: [PATCH] excedence -> excess --- .../dama/classical_pointfree/ordered_sets.ma | 8 +- .../matita/dama/{excedence.ma => excess.ma} | 74 +++++----- helm/software/matita/dama/group.ma | 2 +- helm/software/matita/dama/lattice.ma | 10 +- helm/software/matita/dama/ordered_group.ma | 4 +- helm/software/matita/dama/sequence.ma | 132 +++++++++--------- 6 files changed, 115 insertions(+), 115 deletions(-) rename helm/software/matita/dama/{excedence.ma => excess.ma} (75%) diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma index b42a8c44b..5d9c2da67 100644 --- a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma +++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma @@ -14,9 +14,9 @@ set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/". -include "excedence.ma". +include "excess.ma". -record is_dedekind_sigma_complete (O:excedence) : Type ≝ +record is_dedekind_sigma_complete (O:excess) : Type ≝ { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s); dsc_inf_proof_irrelevant: ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'. @@ -30,7 +30,7 @@ record is_dedekind_sigma_complete (O:excedence) : Type ≝ }. record dedekind_sigma_complete_ordered_set : Type ≝ - { dscos_ordered_set:> excedence; + { dscos_ordered_set:> excess; dscos_dedekind_sigma_complete_properties:> is_dedekind_sigma_complete dscos_ordered_set }. @@ -155,7 +155,7 @@ lemma inf_respects_le: qed. definition is_sequentially_monotone ≝ - λO:excedence.λf:O→O. + λO:excess.λf:O→O. ∀a:nat→O.∀p:is_increasing ? a. is_increasing ? (λi.f (a i)). diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excess.ma similarity index 75% rename from helm/software/matita/dama/excedence.ma rename to helm/software/matita/dama/excess.ma index fa6848e12..827aaf605 100644 --- a/helm/software/matita/dama/excedence.ma +++ b/helm/software/matita/dama/excess.ma @@ -12,27 +12,27 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/excedence/". +set "baseuri" "cic:/matita/excess/". include "higher_order_defs/relations.ma". include "nat/plus.ma". include "constructive_connectives.ma". include "constructive_higher_order_relations.ma". -record excedence : Type ≝ { +record excess : Type ≝ { exc_carr:> Type; exc_relation: exc_carr → exc_carr → Type; exc_coreflexive: coreflexive ? exc_relation; exc_cotransitive: cotransitive ? exc_relation }. -interpretation "excedence" 'nleq a b = - (cic:/matita/excedence/exc_relation.con _ a b). +interpretation "excess" 'nleq a b = + (cic:/matita/excess/exc_relation.con _ a b). -definition le ≝ λE:excedence.λa,b:E. ¬ (a ≰ b). +definition le ≝ λE:excess.λa,b:E. ¬ (a ≰ b). interpretation "ordered sets less or equal than" 'leq a b = - (cic:/matita/excedence/le.con _ a b). + (cic:/matita/excess/le.con _ a b). lemma le_reflexive: ∀E.reflexive ? (le E). intros (E); unfold; cases E; simplify; intros (x); apply (H x); @@ -53,13 +53,13 @@ record apartness : Type ≝ { notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}. interpretation "apartness" 'apart x y = - (cic:/matita/excedence/ap_apart.con _ x y). + (cic:/matita/excess/ap_apart.con _ x y). definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. -definition apart ≝ λE:excedence.λa,b:E. a ≰ b ∨ b ≰ a. +definition apart ≝ λE:excess.λa,b:E. a ≰ b ∨ b ≰ a. -definition apart_of_excedence: excedence → apartness. +definition apart_of_excess: excess → apartness. intros (E); apply (mk_apartness E (apart E)); [1: unfold; cases E; simplify; clear E; intros (x); unfold; intros (H1); apply (H x); cases H1; assumption; @@ -69,13 +69,13 @@ intros (E); apply (mk_apartness E (apart E)); [left; left|right; left|right; right|left; right] assumption] qed. -coercion cic:/matita/excedence/apart_of_excedence.con. +coercion cic:/matita/excess/apart_of_excess.con. definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b). notation "a break ≈ b" non associative with precedence 50 for @{ 'napart $a $b}. interpretation "alikeness" 'napart a b = - (cic:/matita/excedence/eq.con _ a b). + (cic:/matita/excess/eq.con _ a b). lemma eq_reflexive:∀E. reflexive ? (eq E). intros (E); unfold; intros (x); apply ap_coreflexive; @@ -88,7 +88,7 @@ qed. lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_. -coercion cic:/matita/excedence/eq_sym.con. +coercion cic:/matita/excess/eq_sym.con. lemma eq_trans_: ∀E.transitive ? (eq E). (* bug. intros k deve fare whd quanto basta *) @@ -103,7 +103,7 @@ notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}. interpretation "eq_rew" 'eqrewrite = - (cic:/matita/excedence/eq_trans.con _ _ _). + (cic:/matita/excess/eq_trans.con _ _ _). (* BUG: vedere se ricapita *) alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con". @@ -112,10 +112,10 @@ intros 5 (E x y Lxy Lyx); intro H; cases H; [apply Lxy;|apply Lyx] assumption; qed. -definition lt ≝ λE:excedence.λa,b:E. a ≤ b ∧ a # b. +definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b. interpretation "ordered sets less than" 'lt a b = - (cic:/matita/excedence/lt.con _ a b). + (cic:/matita/excess/lt.con _ a b). lemma lt_coreflexive: ∀E.coreflexive ? (lt E). intros 2 (E x); intro H; cases H (_ ABS); @@ -132,36 +132,36 @@ lapply (exc_coreflexive E) as r; unfold coreflexive in r; |2: lapply (c ?? x H2) as H3; cases H3 (H4 H4); [right; assumption|cases (Lxy H4)]] qed. -theorem lt_to_excede: ∀E:excedence.∀a,b:E. (a < b) → (b ≰ a). +theorem lt_to_excede: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a). intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *) qed. -lemma unfold_apart: ∀E:excedence. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y. +lemma unfold_apart: ∀E:excess. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y. intros; assumption; qed. -lemma le_rewl: ∀E:excedence.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z. +lemma le_rewl: ∀E:excess.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z. intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz); intro Xyz; apply Exy; apply unfold_apart; right; assumption; qed. notation > "'Ex'≪" non associative with precedence 50 for - @{'excedencerewritel}. + @{'excessrewritel}. -interpretation "exc_rewl" 'excedencerewritel = - (cic:/matita/excedence/exc_rewl.con _ _ _). +interpretation "exc_rewl" 'excessrewritel = + (cic:/matita/excess/exc_rewl.con _ _ _). -lemma le_rewr: ∀E:excedence.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y. +lemma le_rewr: ∀E:excess.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y. intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz); intro Xyz; apply Exy; apply unfold_apart; left; assumption; qed. notation > "'Ex'≫" non associative with precedence 50 for - @{'excedencerewriter}. + @{'excessrewriter}. -interpretation "exc_rewr" 'excedencerewriter = - (cic:/matita/excedence/exc_rewr.con _ _ _). +interpretation "exc_rewr" 'excessrewriter = + (cic:/matita/excess/exc_rewr.con _ _ _). lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z. intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption] @@ -173,53 +173,53 @@ intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); apply ap_symmetric; assumption; qed. -lemma exc_rewl: ∀A:excedence.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. +lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption] cases Exy; right; assumption; qed. -lemma exc_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x. +lemma exc_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x. intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption] elim (Exy); left; assumption; qed. -lemma lt_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z < y → z < x. +lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x. intros (A x y z E H); split; elim H; [apply (le_rewr ???? (eq_sym ??? E));|apply (ap_rewr ???? E)] assumption; qed. -lemma lt_rewl: ∀A:excedence.∀x,z,y:A. x ≈ y → y < z → x < z. +lemma lt_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y < z → x < z. intros (A x y z E H); split; elim H; [apply (le_rewl ???? (eq_sym ??? E));| apply (ap_rewl ???? E);] assumption; qed. -lemma lt_le_transitive: ∀A:excedence.∀x,y,z:A.x < y → y ≤ z → x < z. +lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z. intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)] whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)] cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)] right; assumption; qed. -lemma le_lt_transitive: ∀A:excedence.∀x,y,z:A.x ≤ y → y < z → x < z. +lemma le_lt_transitive: ∀A:excess.∀x,y,z:A.x ≤ y → y < z → x < z. intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)] whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)] cases (exc_cotransitive ??? x EXx) (EXz EXz); [right; assumption] cases LE; assumption; qed. -lemma le_le_eq: ∀E:excedence.∀a,b:E. a ≤ b → b ≤ a → a ≈ b. +lemma le_le_eq: ∀E:excess.∀a,b:E. a ≤ b → b ≤ a → a ≈ b. intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption; qed. -lemma eq_le_le: ∀E:excedence.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a. -intros (E x y H); unfold apart_of_excedence in H; unfold apart in H; +lemma eq_le_le: ∀E:excess.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a. +intros (E x y H); unfold apart_of_excess in H; unfold apart in H; simplify in H; split; intro; apply H; [left|right] assumption. qed. -lemma ap_le_to_lt: ∀E:excedence.∀a,c:E.c # a → c ≤ a → c < a. +lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a. intros; split; assumption; qed. -definition total_order_property : ∀E:excedence. Type ≝ - λE:excedence. ∀a,b:E. a ≰ b → b < a. +definition total_order_property : ∀E:excess. Type ≝ + λE:excess. ∀a,b:E. a ≰ b → b < a. diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma index b298e82e0..0e2668c2d 100644 --- a/helm/software/matita/dama/group.ma +++ b/helm/software/matita/dama/group.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/group/". -include "excedence.ma". +include "excess.ma". definition left_neutral ≝ λC:apartness.λop.λe:C. ∀x:C. op e x ≈ x. definition right_neutral ≝ λC:apartness.λop. λe:C. ∀x:C. op x e ≈ x. diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma index d6b637a0d..768c86df1 100644 --- a/helm/software/matita/dama/lattice.ma +++ b/helm/software/matita/dama/lattice.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/lattice/". -include "excedence.ma". +include "excess.ma". record lattice : Type ≝ { l_carr:> apartness; @@ -40,8 +40,8 @@ interpretation "Lattice join" 'or a b = definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b). -lemma excedence_of_lattice: lattice → excedence. -intro l; apply (mk_excedence l (excl l)); +lemma excess_of_lattice: lattice → excess. +intro l; apply (mk_excess l (excl l)); [ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x); apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption; | intros 3 (x y z); unfold excl; intro H; @@ -55,7 +55,7 @@ intro l; apply (mk_excedence l (excl l)); assumption] qed. -coercion cic:/matita/lattice/excedence_of_lattice.con. +coercion cic:/matita/lattice/excess_of_lattice.con. lemma feq_ml: ∀ml: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 ⊢ %; @@ -69,7 +69,7 @@ qed. lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b). intros (l a b H); - unfold le in H; unfold excedence_of_lattice in H; + unfold le in H; unfold excess_of_lattice in H; unfold excl in H; simplify in H; unfold eq; assumption; qed. diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma index e6b6f55ef..a00b6eb4a 100644 --- a/helm/software/matita/dama/ordered_group.ma +++ b/helm/software/matita/dama/ordered_group.ma @@ -18,8 +18,8 @@ include "group.ma". record pogroup_ : Type ≝ { og_abelian_group_: abelian_group; - og_excedence:> excedence; - og_with: carr og_abelian_group_ = apart_of_excedence og_excedence + og_excess:> excess; + og_with: carr og_abelian_group_ = apart_of_excess og_excess }. lemma og_abelian_group: pogroup_ → abelian_group. diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma index c26ae5721..9990f8c7d 100644 --- a/helm/software/matita/dama/sequence.ma +++ b/helm/software/matita/dama/sequence.ma @@ -14,46 +14,46 @@ set "baseuri" "cic:/matita/sequence/". -include "excedence.ma". +include "excess.ma". -definition sequence := λO:excedence.nat → O. +definition sequence := λO:excess.nat → O. -definition fun_of_sequence: ∀O:excedence.sequence O → nat → O. +definition fun_of_sequence: ∀O:excess.sequence O → nat → O. intros; apply s; assumption; qed. coercion cic:/matita/sequence/fun_of_sequence.con 1. definition upper_bound ≝ - λO:excedence.λa:sequence O.λu:O.∀n:nat.a n ≤ u. + λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u. definition lower_bound ≝ - λO:excedence.λa:sequence O.λu:O.∀n:nat.u ≤ a n. + λO:excess.λa:sequence O.λu:O.∀n:nat.u ≤ a n. definition strong_sup ≝ - λO:excedence.λs:sequence O.λx. + λO:excess.λs:sequence O.λx. upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y). definition strong_inf ≝ - λO:excedence.λs:sequence O.λx. + λO:excess.λs:sequence O.λx. lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n). definition weak_sup ≝ - λO:excedence.λs:sequence O.λx. + λO:excess.λs:sequence O.λx. upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y). definition weak_inf ≝ - λO:excedence.λs:sequence O.λx. + λO:excess.λs:sequence O.λx. lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x). lemma strong_sup_is_weak: - ∀O:excedence.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x. + ∀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:excedence.∀s:sequence O.∀x:O.strong_inf ? s x → weak_inf ? s x. + ∀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. @@ -66,169 +66,169 @@ definition tends0 ≝ ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e. definition increasing ≝ - λO:excedence.λa:sequence O.∀n:nat.a n ≤ a (S n). + λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n). definition decreasing ≝ - λO:excedence.λa:sequence O.∀n:nat.a (S n) ≤ a n. + λO:excess.λa:sequence O.∀n:nat.a (S n) ≤ a n. (* -definition is_upper_bound ≝ λO:excedence.λa:sequence O.λu:O.∀n:nat.a n ≤ u. -definition is_lower_bound ≝ λO:excedence.λa:sequence O.λu:O.∀n:nat.u ≤ 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:excedence) (a:sequence O) (u:O) : Prop ≝ +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:excedence) (a:sequence O) (u:O) : Prop ≝ +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:excedence) (a:sequence O) : Type ≝ +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:excedence) (a:sequence O) : Type ≝ +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:excedence) (a:sequence O) : Type ≝ +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:excedence) : Type ≝ +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:excedence) : Type ≝ +record bounded_above_sequence (O:excess) : Type ≝ { bas_seq:> sequence O; bas_is_bounded_above:> is_bounded_above ? bas_seq }. -record bounded_sequence (O:excedence) : Type ≝ +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:excedence.λb:bounded_sequence O. + λ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:excedence.λb:bounded_sequence O. + λ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:excedence.λb:bounded_below_sequence O. + λO:excess.λb:bounded_below_sequence O. ib_lower_bound ? b (bbs_is_bounded_below ? b). lemma lower_bound_is_lower_bound: - ∀O:excedence.∀b:bounded_below_sequence O. + ∀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:excedence.λb:bounded_above_sequence O. + λO:excess.λb:bounded_above_sequence O. ib_upper_bound ? b (bas_is_bounded_above ? b). lemma upper_bound_is_upper_bound: - ∀O:excedence.∀b:bounded_above_sequence O. + ∀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_excedence: excedence → excedence. -intros (E); apply (mk_excedence E); [apply (λx,y.exc_relation E y x)] +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_excedence: excedence → excedence. -intros (p); apply (mk_excedence (reverse_excedence p)); -generalize in match (reverse_excedence p); intros (E); +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:excedence.∀a:sequence O.∀l:O. - is_lower_bound O a l → is_upper_bound (reverse_excedence O) a l. -intros (O a l H); unfold; intros (n); unfold reverse_excedence; -unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H; + ∀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:excedence.∀a:sequence O.∀l:O. - is_upper_bound O a l → is_lower_bound (reverse_excedence O) a l. -intros (O a l H); unfold; intros (n); unfold reverse_excedence; -unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H; + ∀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:excedence.∀a:sequence O.∀l:O. - is_lower_bound (reverse_excedence O) a l → is_upper_bound O a l. -intros (O a l H); unfold; intros (n); unfold reverse_excedence in H; -unfold reverse_excedence in H; simplify in H; apply H; + ∀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:excedence.∀a:sequence O.∀l:O. - is_upper_bound (reverse_excedence O) a l → is_lower_bound O a l. -intros (O a l H); unfold; intros (n); unfold reverse_excedence in H; -unfold reverse_excedence in H; simplify in H; apply H; + ∀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:excedence.∀a:bounded_below_sequence O.∀l:O. - is_inf O a l → is_sup (reverse_excedence O) a l. -intros (O a l H); apply (mk_is_sup (reverse_excedence O)); + ∀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_excedence; simplify; unfold reverse_excedence; simplify; +|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:excedence.∀a:bounded_above_sequence O.∀l:O. - is_sup O a l → is_inf (reverse_excedence O) a l. -intros (O a l H); apply (mk_is_inf (reverse_excedence O)); + ∀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_excedence; simplify; unfold reverse_excedence; simplify; +|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:excedence.∀a:bounded_above_sequence O.∀l:O. - is_sup (reverse_excedence O) a l → is_inf O a l. + ∀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_excedence O)); assumption -|2: intros (v H1); apply (sup_least_upper_bound (reverse_excedence O) a l H v); + 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:excedence.∀a:bounded_above_sequence O.∀l:O. - is_inf (reverse_excedence O) a l → is_sup O a l. + ∀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_excedence O)); assumption -|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_excedence O) a l H v); + 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. -- 2.39.2