right; assumption;
qed.
+lemma le_le_eq: ∀E:excedence.∀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.
\ No newline at end of file
interpretation "Lattice join" 'or a b =
(cic:/matita/lattice/join.con _ a b).
-(*
-include "ordered_set.ma".
-
-record lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? join;
- l_associative_j: associative ? join;
- l_comm_m: symmetric ? meet;
- l_associative_m: associative ? meet;
- (* other properties *)
- l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
- l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
- }.
-
-record lattice : Type \def
- { l_carrier:> Type;
- l_join: l_carrier→l_carrier→l_carrier;
- l_meet: l_carrier→l_carrier→l_carrier;
- l_lattice_properties:> is_lattice ? l_join l_meet
- }.
-
-definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
-
-definition ordered_set_of_lattice: lattice → ordered_set.
- intros (L);
- apply mk_ordered_set;
- [2: apply (le L)
- | skip
- | apply mk_is_order_relation;
- [ unfold reflexive;
- intros;
- unfold;
- rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
- rewrite > l_adsorb_m_j;
- [ reflexivity
- | apply (l_lattice_properties L)
- ]
- | intros;
- unfold transitive;
- unfold le;
- intros;
- rewrite < H;
- rewrite > (l_associative_m ? ? ? L);
- rewrite > H1;
- reflexivity
- | unfold antisimmetric;
- unfold le;
- intros;
- rewrite < H;
- rewrite > (l_comm_m ? ? ? L);
- assumption
- ]
- ]
-qed.
-
-coercion cic:/matita/lattices/ordered_set_of_lattice.con.
-*)
+definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
+
+lemma excedence_of_lattice: lattice → excedence.
+intro l; apply (mk_excedence 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;
+ cases (ap_cotransitive ??? (x∧z∧y) H) (H1 H2); [2:
+ left; apply ap_symmetric; apply (strong_extm ? y);
+ apply (ap_rewl ???? (meet_comm ???));
+ apply (ap_rewr ???? (meet_comm ???));
+ assumption]
+ cases (ap_cotransitive ??? (x∧z) H1) (H2 H3); [left; assumption]
+ right; apply (strong_extm ? x); apply (ap_rewr ???? (meet_assoc ????));
+ assumption]
+qed.
+
+coercion cic:/matita/lattice/excedence_of_lattice.con.
\ No newline at end of file
include "metric_space.ma".
include "lattice.ma".
-record mlattice (R : ogroup) : Type ≝ {
+record mlattice_ (R : ogroup) : Type ≝ {
ml_mspace_: metric_space R;
ml_lattice:> lattice;
ml_with_: ms_carr ? ml_mspace_ = ap_carr (l_carr ml_lattice)
}.
-lemma ml_mspace: ∀R.mlattice R → metric_space R.
-intros (R ml); apply (mk_metric_space R ml); unfold Type_OF_mlattice;
+lemma ml_mspace: ∀R.mlattice_ R → metric_space R.
+intros (R ml); apply (mk_metric_space R 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));
qed.
coercion cic:/matita/metric_lattice/ml_mspace.con.
+
+record is_mlattice (R : ogroup) (ml: mlattice_ R) : Type ≝ {
+ ml_prop1: ∀a,b:ml. 0 < δ a b → a # b;
+ ml_prop2: ∀a,b,c:ml. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ δ b c
+}.
+
+record mlattice (R : ogroup) : Type ≝ {
+ ml_carr :> mlattice_ R;
+ ml_props:> is_mlattice R ml_carr
+}.
+
+axiom meq_joinl: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δx y ≈ δz y.
+
+lemma meq_joinr: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δy x ≈ δy z.
+intros; apply (eq_trans ???? (msymmetric ??y x));
+apply (eq_trans ????? (msymmetric ??z y)); apply meq_joinl; assumption;
+qed.
+
+(*
+lemma foo: ∀R.∀ml:mlattice R.∀x,y,z:ml. δx y ≈ δ(y∨x) (y∨z).
+intros; apply le_le_eq; [
+ apply (le_rewr ???? (meq_joinl ????? (join_comm ???)));
+ apply (le_rewr ???? (meq_joinr ????? (join_comm ???)));
+*)
+
+(* 3.11 *)
+lemma le_mtri:
+ ∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
+intros (R ml x y z Lxy Lyz); apply le_le_eq; [apply mtineq]
+apply (le_transitive ????? (ml_prop2 ?? ml (y∧x) ??));
+(* auto type. assert failure *)
apply (le_rewr ??? (g) (zero_neutral ??) H);
qed.
+lemma fle_plusr: ∀G:ogroup. ∀f,g,h:G. f≤g → f+h≤g+h.
+intros (G f g h H); apply (le_rewl ???? (plus_comm ???));
+apply (le_rewr ???? (plus_comm ???)); apply fle_plusl; assumption;
+qed.
+
lemma plus_cancl_le:
∀G:ogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y.
intros 5 (G x y z L);
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 tends ≝
+ λO:ogroup.λs:sequence O.
+ ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
definition increasing ≝
λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
projects / helm.git / commitdiff