interpretation "constructive and" 'and x y =
(cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y).
+inductive exT (A:Type) (P:A→Type) : Type ≝
+ ex_introT: ∀w:A. P w → exT A P.
+
inductive ex (A:Type) (P:A→Prop) : Type ≝
ex_intro: ∀w:A. P w → ex A P.
+(*
notation < "hvbox(Σ ident i opt (: ty) break . p)"
right associative with precedence 20
for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p)}
@{\lambda ${ident i} . $p}}}.
+*)
-interpretation "constructive exists" 'sigma \eta.x =
+interpretation "constructive exists" 'exists \eta.x =
(cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
+interpretation "constructive exists (Type)" 'exists \eta.x =
+ (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x).
alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)".
definition Not ≝ λx:Type.x → False.
include "metric_lattice.ma".
include "sequence.ma".
+include "constructive_connectives.ma".
(* Section 3.2 *)
+(* 3.21 *)
+
+
(* 3.17 *)
interpretation "axiomatic apartness" 'apart x y =
(cic:/matita/excedence/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_of_excedence: excedence → apartness.
definition right_neutral ≝ λC:apartness.λop. λe:C. ∀x:C. op x e ≈ x.
definition left_inverse ≝ λC:apartness.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x ≈ e.
definition right_inverse ≝ λC:apartness.λop.λe:C.λ inv: C→ C. ∀x:C. op x (inv x) ≈ e.
-definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
(* ALLOW DEFINITION WITH SOME METAS *)
definition distributive_left ≝
l_carr:> apartness;
join: l_carr → l_carr → l_carr;
meet: l_carr → l_carr → l_carr;
+ join_refl: ∀x.join x x ≈ x;
+ meet_refl: ∀x.meet x x ≈ x;
join_comm: ∀x,y:l_carr. join x y ≈ join y x;
meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z;
meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z;
absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
- absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f
+ absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f;
+ strong_extj: ∀x.strong_ext ? (join x);
+ strong_extm: ∀x.strong_ext ? (meet x)
}.
interpretation "Lattice meet" 'and a b =
apply (lt0plus_orlt ????? LT0); apply mpositive;]
qed.
+coercion cic:/matita/metric_space/apart_of_metric_space.con.
apply (plus_cancr_ap ??? y); apply (ap_rewl ???? (zero_neutral ??));
assumption;
qed.
+
+lemma le0plus_le:
+ ∀G:ogroup.∀a,b,c:G. 0 ≤ b → a + b ≤ c → a ≤ c.
+intros (G a b c L H); apply (le_transitive ????? H);
+apply (plus_cancl_le ??? (-a));
+apply (le_rewl ??? 0 (opp_inverse ??));
+apply (le_rewr ??? (-a + a + b) (plus_assoc ????));
+apply (le_rewr ??? (0 + b) (opp_inverse ??));
+apply (le_rewr ??? b (zero_neutral ??));
+assumption;
+qed.
+
+
+
+
+
\ No newline at end of file
lemma lattice_of_pmlattice: ∀R: ogroup. pmlattice R → lattice.
intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml));
-[apply (join ? pml)|apply (meet ? pml)]
-intros (x y z); whd; intro H; whd in H; cases H (LE AP);
-[apply (prop2a ? pml pml x y); |apply (prop2b ? pml pml x y);
+[apply (join ? pml)|apply (meet ? pml)
+|3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);]
+[apply (prop1b ? pml pml x); |apply (prop1a ? pml pml x);
+|apply (prop2a ? pml pml x y); |apply (prop2b ? pml pml x y);
|apply (prop3a ? pml pml x y z);|apply (prop3b ? pml pml x y z);
|apply (prop4a ? pml pml x y); |apply (prop4b ? pml pml x y);]
-apply ap_symmetric; assumption;
+try (apply ap_symmetric; assumption); intros 4 (x y z H); change with (0 < (δ y z));
+[ change in H with (0 < δ (x ∨ y) (x ∨ z));
+ apply (lt_le_transitive ???? H);
+ apply (le0plus_le ???? (mpositive ? pml ??) (prop5 ? pml pml x y z));
+| change in H with (0 < δ (x ∧ y) (x ∧ z));
+ apply (lt_le_transitive ???? H);
+ apply (le0plus_le ???? (mpositive ? pml (x∨y) (x∨z)));
+ apply (le_rewl ??? ? (plus_comm ???));
+ apply (prop5 ? pml pml);]
qed.
coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.
\ No newline at end of file
coercion cic:/matita/sequence/fun_of_sequence.con 1.
-definition is_increasing ≝ λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
-definition is_decreasing ≝ λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
+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.
+
+
+(*
definition is_upper_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
definition is_lower_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v);
apply is_upper_bound_reverse_is_lower_bound; assumption;]
qed.
+
+*)
\ No newline at end of file
projects / helm.git / commitdiff