From 2114a7d8dcde253a35e9963df34a86376ec24add Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Nov 2007 12:33:14 +0000 Subject: [PATCH] ... --- .../dama/constructive_pointfree/lebesgue.ma | 6 +++ .../matita/dama/{ => doc}/DIMOSTRAZIONE | 0 .../matita/dama/{ => doc}/NotaReticoli.pdf | 0 helm/software/matita/dama/sequence.ma | 40 +++++++++++-------- 4 files changed, 30 insertions(+), 16 deletions(-) rename helm/software/matita/dama/{ => doc}/DIMOSTRAZIONE (100%) rename helm/software/matita/dama/{ => doc}/NotaReticoli.pdf (100%) diff --git a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma index 1eb6e4aac..824202a78 100644 --- a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma +++ b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma @@ -19,3 +19,9 @@ include "sequence.ma". (* Section 3.2 *) +(* 3.17 *) + + +(* 3.20 *) +lemma uniq_sup: ∀O:ogroup.∀s:sequence O.∀x,y:O. is_sup ? s x → is_sup ? s y → x ≈ y. +intros; \ No newline at end of file diff --git a/helm/software/matita/dama/DIMOSTRAZIONE b/helm/software/matita/dama/doc/DIMOSTRAZIONE similarity index 100% rename from helm/software/matita/dama/DIMOSTRAZIONE rename to helm/software/matita/dama/doc/DIMOSTRAZIONE diff --git a/helm/software/matita/dama/NotaReticoli.pdf b/helm/software/matita/dama/doc/NotaReticoli.pdf similarity index 100% rename from helm/software/matita/dama/NotaReticoli.pdf rename to helm/software/matita/dama/doc/NotaReticoli.pdf diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma index 8d3ba44df..2d304d2af 100644 --- a/helm/software/matita/dama/sequence.ma +++ b/helm/software/matita/dama/sequence.ma @@ -16,49 +16,57 @@ set "baseuri" "cic:/matita/sequence/". include "ordered_set.ma". -definition is_increasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n). -definition is_decreasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n. +definition sequence := λO:pordered_set.nat → O. -definition is_upper_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u. -definition is_lower_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n. +definition fun_of_sequence: ∀O:pordered_set.sequence O → nat → O. +intros; apply s; assumption; +qed. + +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 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. -record is_sup (O:pordered_set) (a:nat→O) (u:O) : Prop ≝ +record is_sup (O:pordered_set) (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:pordered_set) (a:nat→O) (u:O) : Prop ≝ +record is_inf (O:pordered_set) (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:pordered_set) (a:nat→O) : Type ≝ +record is_bounded_below (O:pordered_set) (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:pordered_set) (a:nat→O) : Type ≝ +record is_bounded_above (O:pordered_set) (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:pordered_set) (a:nat→O) : Type ≝ +record is_bounded (O:pordered_set) (a:sequence O) : Type ≝ { ib_bounded_below:> is_bounded_below ? a; ib_bounded_above:> is_bounded_above ? a }. record bounded_below_sequence (O:pordered_set) : Type ≝ - { bbs_seq:1> nat→O; + { bbs_seq:> sequence O; bbs_is_bounded_below:> is_bounded_below ? bbs_seq }. record bounded_above_sequence (O:pordered_set) : Type ≝ - { bas_seq:1> nat→O; + { bas_seq:> sequence O; bas_is_bounded_above:> is_bounded_above ? bas_seq }. record bounded_sequence (O:pordered_set) : Type ≝ - { bs_seq:1> nat → O; + { bs_seq:> sequence O; bs_is_bounded_below: is_bounded_below ? bs_seq; bs_is_bounded_above: is_bounded_above ? bs_seq }. @@ -110,28 +118,28 @@ apply mk_is_porder_relation; qed. lemma is_lower_bound_reverse_is_upper_bound: - ∀O:pordered_set.∀a:nat→O.∀l:O. + ∀O:pordered_set.∀a:sequence O.∀l:O. is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l. intros (O a l H); unfold; intros (n); unfold reverse_pordered_set; unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H; qed. lemma is_upper_bound_reverse_is_lower_bound: - ∀O:pordered_set.∀a:nat→O.∀l:O. + ∀O:pordered_set.∀a:sequence O.∀l:O. is_upper_bound O a l → is_lower_bound (reverse_pordered_set O) a l. intros (O a l H); unfold; intros (n); unfold reverse_pordered_set; unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H; qed. lemma reverse_is_lower_bound_is_upper_bound: - ∀O:pordered_set.∀a:nat→O.∀l:O. + ∀O:pordered_set.∀a:sequence O.∀l:O. is_lower_bound (reverse_pordered_set O) a l → is_upper_bound O a l. intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H; unfold reverse_excedence in H; simplify in H; apply H; qed. lemma reverse_is_upper_bound_is_lower_bound: - ∀O:pordered_set.∀a:nat→O.∀l:O. + ∀O:pordered_set.∀a:sequence O.∀l:O. is_upper_bound (reverse_pordered_set O) a l → is_lower_bound O a l. intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H; unfold reverse_excedence in H; simplify in H; apply H; -- 2.39.2