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:
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:
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.
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 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.
+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.
{ 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 ≝
{ 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 ≝
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 ≝
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 ≝
mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
definition lower_bound ≝
mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
definition lower_bound ≝
is_lower_bound ? b (lower_bound ? b).
intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
qed.
definition upper_bound ≝
is_lower_bound ? b (lower_bound ? b).
intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
qed.
definition upper_bound ≝
is_upper_bound ? b (upper_bound ? b).
intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
qed.
is_upper_bound ? b (upper_bound ? b).
intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
qed.
-definition reverse_pordered_set: pordered_set → pordered_set.
-intros (p); apply (mk_pordered_set (reverse_excedence p));
+definition reverse_excedence: excedence → excedence.
+intros (p); apply (mk_excedence (reverse_excedence p));
generalize in match (reverse_excedence 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:
generalize in match (reverse_excedence 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: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;
+ ∀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;
qed.
lemma is_upper_bound_reverse_is_lower_bound:
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: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;
+ ∀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;
qed.
lemma reverse_is_lower_bound_is_upper_bound:
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: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;
+ ∀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;
- ∀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;
+ ∀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;
- ∀O:pordered_set.∀a:bounded_below_sequence O.∀l:O.
- is_inf O a l → is_sup (reverse_pordered_set O) a l.
-intros (O a l H); apply (mk_is_sup (reverse_pordered_set O));
+ ∀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:pordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_sup O a l → is_inf (reverse_pordered_set O) a l.
-intros (O a l H); apply (mk_is_inf (reverse_pordered_set O));
+ ∀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:pordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_sup (reverse_pordered_set O) a l → is_inf O a l.
+ ∀O:excedence.∀a:bounded_above_sequence O.∀l:O.
+ is_sup (reverse_excedence O) a l → is_inf O a l.
- apply (sup_upper_bound (reverse_pordered_set O)); assumption
-|2: intros (v H1); apply (sup_least_upper_bound (reverse_pordered_set O) a l H v);
+ apply (sup_upper_bound (reverse_excedence O)); assumption
+|2: intros (v H1); apply (sup_least_upper_bound (reverse_excedence O) a l H v);
- ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_inf (reverse_pordered_set O) a l → is_sup O a l.
+ ∀O:excedence.∀a:bounded_above_sequence O.∀l:O.
+ is_inf (reverse_excedence O) a l → is_sup O a l.
- apply (inf_lower_bound (reverse_pordered_set O)); assumption
-|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v);
+ apply (inf_lower_bound (reverse_excedence O)); assumption
+|2: intros (v H1); apply (inf_greatest_lower_bound (reverse_excedence O) a l H v);