--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
+
+include "ordered_sets.ma".
+
+record is_dedekind_sigma_complete (O:ordered_set) : 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'.
+ (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) =
+ (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]);
+ dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s);
+ dsc_sup_proof_irrelevant:
+ ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'.
+ (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) =
+ (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ])
+ }.
+
+record dedekind_sigma_complete_ordered_set : Type ≝
+ { dscos_ordered_set:> ordered_set;
+ dscos_dedekind_sigma_complete_properties:>
+ is_dedekind_sigma_complete dscos_ordered_set
+ }.
+
+definition inf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ bounded_below_sequence O → O.
+ intros;
+ elim
+ (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b);
+ [ apply a
+ | apply (lower_bound ? b)
+ | apply lower_bound_is_lower_bound
+ ]
+qed.
+
+lemma inf_is_inf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a:bounded_below_sequence O.
+ is_inf ? a (inf ? a).
+ intros;
+ unfold inf;
+ simplify;
+ elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a
+(lower_bound O a) (lower_bound_is_lower_bound O a));
+ simplify;
+ assumption.
+qed.
+
+lemma inf_proof_irrelevant:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a,a':bounded_below_sequence O.
+ bbs_seq ? a = bbs_seq ? a' →
+ inf ? a = inf ? a'.
+ intros 3;
+ elim a 0;
+ elim a';
+ simplify in H;
+ generalize in match i1;
+ clear i1;
+ rewrite > H;
+ intro;
+ simplify;
+ rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i)
+ (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i)
+ (ib_lower_bound_is_lower_bound ? f i2));
+ reflexivity.
+qed.
+
+definition sup:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ bounded_above_sequence O → O.
+ intros;
+ elim
+ (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b);
+ [ apply a
+ | apply (upper_bound ? b)
+ | apply upper_bound_is_upper_bound
+ ].
+qed.
+
+lemma sup_is_sup:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a:bounded_above_sequence O.
+ is_sup ? a (sup ? a).
+ intros;
+ unfold sup;
+ simplify;
+ elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a
+(upper_bound O a) (upper_bound_is_upper_bound O a));
+ simplify;
+ assumption.
+qed.
+
+lemma sup_proof_irrelevant:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a,a':bounded_above_sequence O.
+ bas_seq ? a = bas_seq ? a' →
+ sup ? a = sup ? a'.
+ intros 3;
+ elim a 0;
+ elim a';
+ simplify in H;
+ generalize in match i1;
+ clear i1;
+ rewrite > H;
+ intro;
+ simplify;
+ rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2)
+ (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2)
+ (ib_upper_bound_is_upper_bound ? f i));
+ reflexivity.
+qed.
+
+axiom daemon: False.
+
+theorem inf_le_sup:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a:bounded_sequence O. inf ? a ≤ sup ? a.
+ intros (O');
+ apply (or_transitive ? ? O' ? (a O));
+ [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*)
+ | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*)
+ ].
+qed.
+
+lemma inf_respects_le:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a:bounded_below_sequence O.∀m:O.
+ is_upper_bound ? a m → inf ? a ≤ m.
+ intros (O');
+ apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?)));
+ [ apply (bbs_is_bounded_below ? a)
+ | apply (mk_is_bounded_above ? ? m H)
+ | apply inf_le_sup
+ | apply
+ (sup_least_upper_bound ? ? ?
+ (sup_is_sup ? (mk_bounded_sequence O' a a
+ (mk_is_bounded_above O' a m H))));
+ assumption
+ ].
+qed.
+
+definition is_sequentially_monotone ≝
+ λO:ordered_set.λf:O→O.
+ ∀a:nat→O.∀p:is_increasing ? a.
+ is_increasing ? (λi.f (a i)).
+
+record is_order_continuous
+ (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop
+≝
+ { ioc_is_sequentially_monotone: is_sequentially_monotone ? f;
+ ioc_is_upper_bound_f_sup:
+ ∀a:bounded_above_sequence O.
+ is_upper_bound ? (λi.f (a i)) (f (sup ? a));
+ ioc_respects_sup:
+ ∀a:bounded_above_sequence O.
+ is_increasing ? a →
+ f (sup ? a) =
+ sup ? (mk_bounded_above_sequence ? (λi.f (a i))
+ (mk_is_bounded_above ? ? (f (sup ? a))
+ (ioc_is_upper_bound_f_sup a)));
+ ioc_is_lower_bound_f_inf:
+ ∀a:bounded_below_sequence O.
+ is_lower_bound ? (λi.f (a i)) (f (inf ? a));
+ ioc_respects_inf:
+ ∀a:bounded_below_sequence O.
+ is_decreasing ? a →
+ f (inf ? a) =
+ inf ? (mk_bounded_below_sequence ? (λi.f (a i))
+ (mk_is_bounded_below ? ? (f (inf ? a))
+ (ioc_is_lower_bound_f_inf a)))
+ }.
+
+theorem tail_inf_increasing:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a:bounded_below_sequence O.
+ let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in
+ let x ≝ λi.inf ? (y i) in
+ is_increasing ? x.
+ [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
+ simplify;
+ intro;
+ apply (ib_lower_bound_is_lower_bound ? a a)
+ | intros;
+ unfold is_increasing;
+ intro;
+ unfold x in ⊢ (? ? ? %);
+ apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n))));
+ change with (is_lower_bound ? (y (S n)) (inf ? (y n)));
+ unfold is_lower_bound;
+ intro;
+ generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1));
+ (*CSC: coercion per FunClass inserita a mano*)
+ suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H);
+ cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1);
+ [ rewrite < Hcut;
+ assumption
+ | unfold y;
+ simplify;
+ autobatch paramodulation library
+ ]
+ ].
+qed.
+
+definition is_liminf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ bounded_below_sequence O → O → Prop.
+ intros;
+ apply
+ (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t);
+ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
+ simplify;
+ intros;
+ apply (ib_lower_bound_is_lower_bound ? b b).
+qed.
+
+definition liminf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ bounded_sequence O → O.
+ intros;
+ apply
+ (sup ?
+ (mk_bounded_above_sequence ?
+ (λi.inf ?
+ (mk_bounded_below_sequence ?
+ (λj.b (i+j)) ?)) ?));
+ [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
+ simplify;
+ intros;
+ apply (ib_lower_bound_is_lower_bound ? b b)
+ | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b));
+ unfold is_upper_bound;
+ intro;
+ change with
+ (inf O
+ (mk_bounded_below_sequence O (\lambda j:nat.b (n+j))
+ (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j))))
+\leq ib_upper_bound O b b);
+ apply (inf_respects_le O);
+ simplify;
+ intro;
+ apply (ib_upper_bound_is_upper_bound ? b b)
+ ].
+qed.
+
+
+definition reverse_dedekind_sigma_complete_ordered_set:
+ dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set.
+ intros;
+ apply mk_dedekind_sigma_complete_ordered_set;
+ [ apply (reverse_ordered_set d)
+ | elim daemon
+ (*apply mk_is_dedekind_sigma_complete;
+ [ intros;
+ elim (dsc_sup ? ? d a m) 0;
+ [ generalize in match H; clear H;
+ generalize in match m; clear m;
+ elim d;
+ simplify in a1;
+ simplify;
+ change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o));
+ apply (ex_intro ? ? a1);
+ simplify in H1;
+ change in m with (Type_OF_ordered_set ? o);
+ apply (is_sup_to_reverse_is_inf ? ? ? ? H1)
+ | generalize in match H; clear H;
+ generalize in match m; clear m;
+ elim d;
+ simplify;
+ change in t with (Type_OF_ordered_set ? o);
+ simplify in t;
+ apply reverse_is_lower_bound_is_upper_bound;
+ assumption
+ ]
+ | apply is_sup_reverse_is_inf;
+ | apply m
+ |
+ ]*)
+ ].
+qed.
+
+definition reverse_bounded_sequence:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ bounded_sequence O →
+ bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O).
+ intros;
+ apply mk_bounded_sequence;
+ [ apply bs_seq;
+ unfold reverse_dedekind_sigma_complete_ordered_set;
+ simplify;
+ elim daemon
+ | elim daemon
+ | elim daemon
+ ].
+qed.
+
+definition limsup ≝
+ λO:dedekind_sigma_complete_ordered_set.
+ λa:bounded_sequence O.
+ liminf (reverse_dedekind_sigma_complete_ordered_set O)
+ (reverse_bounded_sequence O a).
+
+notation "hvbox(〈a〉)"
+ non associative with precedence 45
+for @{ 'hide_everything_but $a }.
+
+interpretation "mk_bounded_above_sequence" 'hide_everything_but a
+= (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+
+interpretation "mk_bounded_below_sequence" 'hide_everything_but a
+= (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+
+theorem eq_f_sup_sup_f:
+ ∀O':dedekind_sigma_complete_ordered_set.
+ ∀f:O'→O'. ∀H:is_order_continuous ? f.
+ ∀a:bounded_above_sequence O'.
+ ∀p:is_increasing ? a.
+ f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?).
+ [ apply (mk_is_bounded_above ? ? (f (sup ? a)));
+ apply ioc_is_upper_bound_f_sup;
+ assumption
+ | intros;
+ apply ioc_respects_sup;
+ assumption
+ ].
+qed.
+
+theorem eq_f_sup_sup_f':
+ ∀O':dedekind_sigma_complete_ordered_set.
+ ∀f:O'→O'. ∀H:is_order_continuous ? f.
+ ∀a:bounded_above_sequence O'.
+ ∀p:is_increasing ? a.
+ ∀p':is_bounded_above ? (λi.f (a i)).
+ f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p').
+ intros;
+ rewrite > (eq_f_sup_sup_f ? f H a H1);
+ apply sup_proof_irrelevant;
+ reflexivity.
+qed.
+
+theorem eq_f_liminf_sup_f_inf:
+ ∀O':dedekind_sigma_complete_ordered_set.
+ ∀f:O'→O'. ∀H:is_order_continuous ? f.
+ ∀a:bounded_sequence O'.
+ let p1 := ? in
+ f (liminf ? a) =
+ sup ?
+ (mk_bounded_above_sequence ?
+ (λi.f (inf ?
+ (mk_bounded_below_sequence ?
+ (λj.a (i+j))
+ ?)))
+ p1).
+ [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
+ simplify;
+ intro;
+ apply (ib_lower_bound_is_lower_bound ? a a)
+ | apply (mk_is_bounded_above ? ? (f (sup ? a)));
+ unfold is_upper_bound;
+ intro;
+ apply (or_transitive ? ? O' ? (f (a n)));
+ [ generalize in match (ioc_is_lower_bound_f_inf ? ? H);
+ intro H1;
+ simplify in H1;
+ rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %)));
+ apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j))
+(mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O);
+ | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*)
+ ]
+ | intros;
+ unfold liminf;
+ clearbody p1;
+ generalize in match (\lambda n:nat
+.inf_respects_le O'
+ (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j))
+ (mk_is_bounded_below O' (\lambda j:nat.a (plus n j))
+ (ib_lower_bound O' a a)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j))))
+ (ib_upper_bound O' a a)
+ (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1)));
+ intro p2;
+ apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O'
+(\lambda i:nat
+ .inf O'
+ (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
+ (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
+ (ib_lower_bound O' a a)
+ (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
+(mk_is_bounded_above O'
+ (\lambda i:nat
+ .inf O'
+ (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
+ (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
+ (ib_lower_bound O' a a)
+ (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
+ (ib_upper_bound O' a a) p2)));
+ unfold bas_seq;
+ change with
+ (is_increasing ? (\lambda i:nat
+.inf O'
+ (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
+ (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
+ (ib_lower_bound O' a a)
+ (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))));
+ apply tail_inf_increasing
+ ].
+qed.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/classical_pointfree/ordered_sets2".
+
+include "classical_pointfree/ordered_sets.ma".
+
+theorem le_f_inf_inf_f:
+ ∀O':dedekind_sigma_complete_ordered_set.
+ ∀f:O'→O'. ∀H:is_order_continuous ? f.
+ ∀a:bounded_below_sequence O'.
+ let p := ? in
+ f (inf ? a) ≤ inf ? (mk_bounded_below_sequence ? (λi. f (a i)) p).
+ [ apply mk_is_bounded_below;
+ [2: apply ioc_is_lower_bound_f_inf;
+ assumption
+ | skip
+ ]
+ | intros;
+ clearbody p;
+ apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? ?));
+ simplify;
+ intro;
+ letin b := (λi.match i with [ O ⇒ inf ? a | S _ ⇒ a n]);
+ change with (f (b O) ≤ f (b (S O)));
+ apply (ioc_is_sequentially_monotone ? ? H);
+ simplify;
+ clear b;
+ intro;
+ elim n1; simplify;
+ [ apply (inf_lower_bound ? ? ? (inf_is_inf ? ?));
+ | apply (or_reflexive O' ? (dscos_ordered_set O'))
+ ]
+ ].
+qed.
+
+theorem le_to_le_sup_sup:
+ ∀O':dedekind_sigma_complete_ordered_set.
+ ∀a,b:bounded_above_sequence O'.
+ (∀i.a i ≤ b i) → sup ? a ≤ sup ? b.
+ intros;
+ apply (sup_least_upper_bound ? ? ? (sup_is_sup ? a));
+ unfold;
+ intro;
+ apply (or_transitive ? ? O');
+ [2: apply H
+ | skip
+ | apply (sup_upper_bound ? ? ? (sup_is_sup ? b))
+ ].
+qed.
+
+interpretation "mk_bounded_sequence" 'hide_everything_but a
+= (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+
+lemma reduce_bas_seq:
+ ∀O:ordered_set.∀a:nat→O.∀p.∀i.
+ bas_seq ? (mk_bounded_above_sequence ? a p) i = a i.
+ intros;
+ reflexivity.
+qed.
+
+(*lemma reduce_bbs_seq:
+ ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
+ bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i.
+ intros;
+ reflexivity.
+qed.*)
+
+axiom inf_extensional:
+ ∀O:dedekind_sigma_complete_ordered_set.
+ ∀a,b:bounded_below_sequence O.
+ (∀i.a i = b i) → inf ? a = inf O b.
+
+lemma eq_to_le: ∀O:ordered_set.∀x,y:O.x=y → x ≤ y.
+ intros;
+ rewrite > H;
+ apply (or_reflexive ? ? O).
+qed.
+
+theorem fatou:
+ ∀O':dedekind_sigma_complete_ordered_set.
+ ∀f:O'→O'. ∀H:is_order_continuous ? f.
+ ∀a:bounded_sequence O'.
+ let pb := ? in
+ let pa := ? in
+ f (liminf ? a) ≤ liminf ? (mk_bounded_sequence ? (λi. f (a i)) pb pa).
+ [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? a);
+ apply mk_is_bounded_above;
+ [2: apply (ioc_is_upper_bound_f_sup ? ? H bas)
+ | skip
+ ]
+ | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? a);
+ apply mk_is_bounded_below;
+ [2: apply (ioc_is_lower_bound_f_inf ? ? H bbs)
+ | skip
+ ]
+ | intros;
+ rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? % ?);
+ [ unfold liminf;
+ apply le_to_le_sup_sup;
+ intro;
+ rewrite > reduce_bas_seq;
+ rewrite > reduce_bas_seq;
+ apply (or_transitive ? ? O');
+ [2: apply le_f_inf_inf_f;
+ assumption
+ | skip
+ | apply eq_to_le;
+ apply inf_extensional;
+ intro;
+ reflexivity
+ ]
+ | assumption
+ ]
+ ].
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/sets/".
+
+include "nat/nat.ma".
+
+definition set ≝ λX:Type.X → Prop.
+
+definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
+
+notation "hvbox(x break ∈ A)" with precedence 60
+for @{ 'member_of $x $A }.
+
+interpretation "Member of" 'member_of x A =
+ (cic:/matita/sets/member_of.con _ A x).
+
+notation "hvbox(x break ∉ A)" with precedence 60
+for @{ 'not_member_of $x $A }.
+
+interpretation "Not member of" 'not_member_of x A =
+ (cic:/matita/logic/connectives/Not.con
+ (cic:/matita/sets/member_of.con _ A x)).
+
+definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False.
+
+notation "∅︀" with precedence 100 for @{ 'emptyset }.
+
+interpretation "Emptyset" 'emptyset =
+ (cic:/matita/sets/emptyset.con _).
+
+definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
+
+notation "hvbox(A break ⊆ B)" with precedence 60
+for @{ 'subset $A $B }.
+
+interpretation "Subset" 'subset A B =
+ (cic:/matita/sets/subset.con _ A B).
+
+definition intersection: ∀X. set X → set X → set X ≝
+ λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
+
+notation "hvbox(A break ∩ B)" with precedence 70
+for @{ 'intersection $A $B }.
+
+interpretation "Intersection" 'intersection A B =
+ (cic:/matita/sets/intersection.con _ A B).
+
+definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
+
+notation "hvbox(A break ∪ B)" with precedence 65
+for @{ 'union $A $B }.
+
+interpretation "Union" 'union A B =
+ (cic:/matita/sets/union.con _ A B).
+
+definition seq ≝ λX:Type.nat → X.
+
+definition nth ≝ λX.λA:seq X.λi.A i.
+
+notation "hvbox(A \sub i)" with precedence 100
+for @{ 'nth $A $i }.
+
+interpretation "nth" 'nth A i =
+ (cic:/matita/sets/nth.con _ A i).
+
+definition countable_union: ∀X. seq (set X) → set X ≝
+ λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
+
+notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
+for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
+
+interpretation "countable_union" 'big_union η.t =
+ (cic:/matita/sets/countable_union.con _ t).
+
+definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
+
+notation "A \sup 'c'" with precedence 100
+for @{ 'complement $A }.
+
+interpretation "Complement" 'complement A =
+ (cic:/matita/sets/complement.con _ A).
+
+definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
+ λX,Y,f,B,x. f x ∈ B.
+
+notation "hvbox(f \sup (-1))" with precedence 100
+for @{ 'finverse $f }.
+
+interpretation "Inverse image" 'finverse f =
+ (cic:/matita/sets/inverse_image.con _ _ f).
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/sigma_algebra/".
+
+include "classical_pointwise/topology.ma".
+
+record is_sigma_algebra (X:Type) (A: set X) (M: set (set X)) : Prop ≝
+ { siga_subset: ∀B.B ∈ M → B ⊆ A;
+ siga_full: A ∈ M;
+ siga_compl: ∀B.B ∈ M → B \sup c ∈ M;
+ siga_enumerable_union:
+ ∀B:seq (set X).(∀i.(B \sub i) ∈ M) → (∪ \sub i B \sub i) ∈ M
+ }.
+
+record sigma_algebra : Type ≝
+ { siga_carrier:> Type;
+ siga_domain:> set siga_carrier;
+ M: set (set siga_carrier);
+ siga_is_sigma_algebra:> is_sigma_algebra ? siga_domain M
+ }.
+
+(*definition is_measurable_map ≝
+ λX:sigma_algebra.λY:topological_space.λf:X → Y.
+ ∀V. V ∈ O Y → f \sup -1 V ∈ M X.*)
+definition is_measurable_map ≝
+ λX:sigma_algebra.λY:topological_space.λf:X → Y.
+ ∀V. V ∈ O Y → inverse_image ? ? f V ∈ M X.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/topology/".
+
+include "classical_pointwise/sets.ma".
+
+record is_topology (X) (A: set X) (O: set (set X)) : Prop ≝
+ { top_subset: ∀B. B ∈ O → B ⊆ A;
+ top_empty: ∅︀ ∈ O;
+ top_full: A ∈ O;
+ top_intersection: ∀B,C. B ∈ O → C ∈ O → B ∩ C ∈ O;
+ top_countable_union:
+ ∀B.(∀i.(B \sub i) ∈ O) → (∪ \sub i (B \sub i)) ∈ O
+ }.
+
+record topological_space : Type ≝
+ { top_carrier:> Type;
+ top_domain:> set top_carrier;
+ O: set (set top_carrier);
+ top_is_topological_space:> is_topology ? top_domain O
+ }.
+
+(*definition is_continuous_map ≝
+ λX,Y: topological_space.λf: X → Y.
+ ∀V. V ∈ O Y → (f \sup -1) V ∈ O X.*)
+definition is_continuous_map ≝
+ λX,Y: topological_space.λf: X → Y.
+ ∀V. V ∈ O Y → inverse_image ? ? f V ∈ O X.
+
+record continuous_map (X,Y: topological_space) : Type ≝
+ { cm_f:> X → Y;
+ cm_is_continuous_map: is_continuous_map ? ? cm_f
+ }.
set "baseuri" "cic:/matita/ordered_groups/".
include "groups.ma".
-include "ordered_sets2.ma".
+include "ordered_sets.ma".
record pre_ordered_abelian_group : Type ≝
{ og_abelian_group:> abelian_group;
apply ib_upper_bound_is_upper_bound.
qed.
-record is_dedekind_sigma_complete (O:ordered_set) : 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'.
- (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) =
- (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]);
- dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s);
- dsc_sup_proof_irrelevant:
- ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'.
- (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) =
- (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ])
- }.
-
-record dedekind_sigma_complete_ordered_set : Type ≝
- { dscos_ordered_set:> ordered_set;
- dscos_dedekind_sigma_complete_properties:>
- is_dedekind_sigma_complete dscos_ordered_set
- }.
-
-definition inf:
- ∀O:dedekind_sigma_complete_ordered_set.
- bounded_below_sequence O → O.
- intros;
- elim
- (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b);
- [ apply a
- | apply (lower_bound ? b)
- | apply lower_bound_is_lower_bound
- ]
-qed.
-
-lemma inf_is_inf:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a:bounded_below_sequence O.
- is_inf ? a (inf ? a).
- intros;
- unfold inf;
- simplify;
- elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a
-(lower_bound O a) (lower_bound_is_lower_bound O a));
- simplify;
- assumption.
-qed.
-
-lemma inf_proof_irrelevant:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a,a':bounded_below_sequence O.
- bbs_seq ? a = bbs_seq ? a' →
- inf ? a = inf ? a'.
- intros 3;
- elim a 0;
- elim a';
- simplify in H;
- generalize in match i1;
- clear i1;
- rewrite > H;
- intro;
- simplify;
- rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i)
- (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i)
- (ib_lower_bound_is_lower_bound ? f i2));
- reflexivity.
-qed.
-
-definition sup:
- ∀O:dedekind_sigma_complete_ordered_set.
- bounded_above_sequence O → O.
- intros;
- elim
- (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b);
- [ apply a
- | apply (upper_bound ? b)
- | apply upper_bound_is_upper_bound
- ].
-qed.
-
-lemma sup_is_sup:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a:bounded_above_sequence O.
- is_sup ? a (sup ? a).
- intros;
- unfold sup;
- simplify;
- elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a
-(upper_bound O a) (upper_bound_is_upper_bound O a));
- simplify;
- assumption.
-qed.
-
-lemma sup_proof_irrelevant:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a,a':bounded_above_sequence O.
- bas_seq ? a = bas_seq ? a' →
- sup ? a = sup ? a'.
- intros 3;
- elim a 0;
- elim a';
- simplify in H;
- generalize in match i1;
- clear i1;
- rewrite > H;
- intro;
- simplify;
- rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2)
- (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2)
- (ib_upper_bound_is_upper_bound ? f i));
- reflexivity.
-qed.
-
-axiom daemon: False.
-
-theorem inf_le_sup:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a:bounded_sequence O. inf ? a ≤ sup ? a.
- intros (O');
- apply (or_transitive ? ? O' ? (a O));
- [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*)
- | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*)
- ].
-qed.
-
-lemma inf_respects_le:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a:bounded_below_sequence O.∀m:O.
- is_upper_bound ? a m → inf ? a ≤ m.
- intros (O');
- apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?)));
- [ apply (bbs_is_bounded_below ? a)
- | apply (mk_is_bounded_above ? ? m H)
- | apply inf_le_sup
- | apply
- (sup_least_upper_bound ? ? ?
- (sup_is_sup ? (mk_bounded_sequence O' a a
- (mk_is_bounded_above O' a m H))));
- assumption
- ].
-qed.
-
-definition is_sequentially_monotone ≝
- λO:ordered_set.λf:O→O.
- ∀a:nat→O.∀p:is_increasing ? a.
- is_increasing ? (λi.f (a i)).
-
-record is_order_continuous
- (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop
-≝
- { ioc_is_sequentially_monotone: is_sequentially_monotone ? f;
- ioc_is_upper_bound_f_sup:
- ∀a:bounded_above_sequence O.
- is_upper_bound ? (λi.f (a i)) (f (sup ? a));
- ioc_respects_sup:
- ∀a:bounded_above_sequence O.
- is_increasing ? a →
- f (sup ? a) =
- sup ? (mk_bounded_above_sequence ? (λi.f (a i))
- (mk_is_bounded_above ? ? (f (sup ? a))
- (ioc_is_upper_bound_f_sup a)));
- ioc_is_lower_bound_f_inf:
- ∀a:bounded_below_sequence O.
- is_lower_bound ? (λi.f (a i)) (f (inf ? a));
- ioc_respects_inf:
- ∀a:bounded_below_sequence O.
- is_decreasing ? a →
- f (inf ? a) =
- inf ? (mk_bounded_below_sequence ? (λi.f (a i))
- (mk_is_bounded_below ? ? (f (inf ? a))
- (ioc_is_lower_bound_f_inf a)))
- }.
-
-theorem tail_inf_increasing:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a:bounded_below_sequence O.
- let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in
- let x ≝ λi.inf ? (y i) in
- is_increasing ? x.
- [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
- simplify;
- intro;
- apply (ib_lower_bound_is_lower_bound ? a a)
- | intros;
- unfold is_increasing;
- intro;
- unfold x in ⊢ (? ? ? %);
- apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n))));
- change with (is_lower_bound ? (y (S n)) (inf ? (y n)));
- unfold is_lower_bound;
- intro;
- generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1));
- (*CSC: coercion per FunClass inserita a mano*)
- suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H);
- cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1);
- [ rewrite < Hcut;
- assumption
- | unfold y;
- simplify;
- autobatch paramodulation library
- ]
- ].
-qed.
-
-definition is_liminf:
- ∀O:dedekind_sigma_complete_ordered_set.
- bounded_below_sequence O → O → Prop.
- intros;
- apply
- (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t);
- apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
- simplify;
- intros;
- apply (ib_lower_bound_is_lower_bound ? b b).
-qed.
+definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
-definition liminf:
- ∀O:dedekind_sigma_complete_ordered_set.
- bounded_sequence O → O.
- intros;
- apply
- (sup ?
- (mk_bounded_above_sequence ?
- (λi.inf ?
- (mk_bounded_below_sequence ?
- (λj.b (i+j)) ?)) ?));
- [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
- simplify;
- intros;
- apply (ib_lower_bound_is_lower_bound ? b b)
- | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b));
- unfold is_upper_bound;
- intro;
- change with
- (inf O
- (mk_bounded_below_sequence O (\lambda j:nat.b (n+j))
- (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b)
- (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j))))
-\leq ib_upper_bound O b b);
- apply (inf_respects_le O);
- simplify;
- intro;
- apply (ib_upper_bound_is_upper_bound ? b b)
- ].
-qed.
+interpretation "Ordered set lt" 'lt a b =
+ (cic:/matita/ordered_sets/lt.con _ a b).
definition reverse_ordered_set: ordered_set → ordered_set.
intros;
].
qed.
-
-definition reverse_dedekind_sigma_complete_ordered_set:
- dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set.
- intros;
- apply mk_dedekind_sigma_complete_ordered_set;
- [ apply (reverse_ordered_set d)
- | elim daemon
- (*apply mk_is_dedekind_sigma_complete;
- [ intros;
- elim (dsc_sup ? ? d a m) 0;
- [ generalize in match H; clear H;
- generalize in match m; clear m;
- elim d;
- simplify in a1;
- simplify;
- change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o));
- apply (ex_intro ? ? a1);
- simplify in H1;
- change in m with (Type_OF_ordered_set ? o);
- apply (is_sup_to_reverse_is_inf ? ? ? ? H1)
- | generalize in match H; clear H;
- generalize in match m; clear m;
- elim d;
- simplify;
- change in t with (Type_OF_ordered_set ? o);
- simplify in t;
- apply reverse_is_lower_bound_is_upper_bound;
- assumption
- ]
- | apply is_sup_reverse_is_inf;
- | apply m
- |
- ]*)
- ].
-qed.
-
-definition reverse_bounded_sequence:
- ∀O:dedekind_sigma_complete_ordered_set.
- bounded_sequence O →
- bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O).
- intros;
- apply mk_bounded_sequence;
- [ apply bs_seq;
- unfold reverse_dedekind_sigma_complete_ordered_set;
- simplify;
- elim daemon
- | elim daemon
- | elim daemon
- ].
-qed.
-
-definition limsup ≝
- λO:dedekind_sigma_complete_ordered_set.
- λa:bounded_sequence O.
- liminf (reverse_dedekind_sigma_complete_ordered_set O)
- (reverse_bounded_sequence O a).
-
-notation "hvbox(〈a〉)"
- non associative with precedence 45
-for @{ 'hide_everything_but $a }.
-
-interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
-
-interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
-
-theorem eq_f_sup_sup_f:
- ∀O':dedekind_sigma_complete_ordered_set.
- ∀f:O'→O'. ∀H:is_order_continuous ? f.
- ∀a:bounded_above_sequence O'.
- ∀p:is_increasing ? a.
- f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?).
- [ apply (mk_is_bounded_above ? ? (f (sup ? a)));
- apply ioc_is_upper_bound_f_sup;
- assumption
- | intros;
- apply ioc_respects_sup;
- assumption
- ].
-qed.
-
-theorem eq_f_sup_sup_f':
- ∀O':dedekind_sigma_complete_ordered_set.
- ∀f:O'→O'. ∀H:is_order_continuous ? f.
- ∀a:bounded_above_sequence O'.
- ∀p:is_increasing ? a.
- ∀p':is_bounded_above ? (λi.f (a i)).
- f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p').
- intros;
- rewrite > (eq_f_sup_sup_f ? f H a H1);
- apply sup_proof_irrelevant;
- reflexivity.
-qed.
-
-theorem eq_f_liminf_sup_f_inf:
- ∀O':dedekind_sigma_complete_ordered_set.
- ∀f:O'→O'. ∀H:is_order_continuous ? f.
- ∀a:bounded_sequence O'.
- let p1 := ? in
- f (liminf ? a) =
- sup ?
- (mk_bounded_above_sequence ?
- (λi.f (inf ?
- (mk_bounded_below_sequence ?
- (λj.a (i+j))
- ?)))
- p1).
- [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
- simplify;
- intro;
- apply (ib_lower_bound_is_lower_bound ? a a)
- | apply (mk_is_bounded_above ? ? (f (sup ? a)));
- unfold is_upper_bound;
- intro;
- apply (or_transitive ? ? O' ? (f (a n)));
- [ generalize in match (ioc_is_lower_bound_f_inf ? ? H);
- intro H1;
- simplify in H1;
- rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %)));
- apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j))
-(mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a)
- (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O);
- | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*)
- ]
- | intros;
- unfold liminf;
- clearbody p1;
- generalize in match (\lambda n:nat
-.inf_respects_le O'
- (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j))
- (mk_is_bounded_below O' (\lambda j:nat.a (plus n j))
- (ib_lower_bound O' a a)
- (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j))))
- (ib_upper_bound O' a a)
- (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1)));
- intro p2;
- apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O'
-(\lambda i:nat
- .inf O'
- (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
- (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
- (ib_lower_bound O' a a)
- (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
-(mk_is_bounded_above O'
- (\lambda i:nat
- .inf O'
- (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
- (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
- (ib_lower_bound O' a a)
- (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
- (ib_upper_bound O' a a) p2)));
- unfold bas_seq;
- change with
- (is_increasing ? (\lambda i:nat
-.inf O'
- (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
- (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
- (ib_lower_bound O' a a)
- (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))));
- apply tail_inf_increasing
- ].
-qed.
-
-
-
-
-definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
-
-interpretation "Ordered set lt" 'lt a b =
- (cic:/matita/ordered_sets/lt.con _ a b).
+record cotransitively_ordered_set: Type :=
+ { cos_ordered_set :> ordered_set;
+ cos_cotransitive: cotransitive ? (os_le cos_ordered_set)
+ }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/ordered_sets2".
-
-include "ordered_sets.ma".
-
-theorem le_f_inf_inf_f:
- ∀O':dedekind_sigma_complete_ordered_set.
- ∀f:O'→O'. ∀H:is_order_continuous ? f.
- ∀a:bounded_below_sequence O'.
- let p := ? in
- f (inf ? a) ≤ inf ? (mk_bounded_below_sequence ? (λi. f (a i)) p).
- [ apply mk_is_bounded_below;
- [2: apply ioc_is_lower_bound_f_inf;
- assumption
- | skip
- ]
- | intros;
- clearbody p;
- apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? ?));
- simplify;
- intro;
- letin b := (λi.match i with [ O ⇒ inf ? a | S _ ⇒ a n]);
- change with (f (b O) ≤ f (b (S O)));
- apply (ioc_is_sequentially_monotone ? ? H);
- simplify;
- clear b;
- intro;
- elim n1; simplify;
- [ apply (inf_lower_bound ? ? ? (inf_is_inf ? ?));
- | apply (or_reflexive O' ? (dscos_ordered_set O'))
- ]
- ].
-qed.
-
-theorem le_to_le_sup_sup:
- ∀O':dedekind_sigma_complete_ordered_set.
- ∀a,b:bounded_above_sequence O'.
- (∀i.a i ≤ b i) → sup ? a ≤ sup ? b.
- intros;
- apply (sup_least_upper_bound ? ? ? (sup_is_sup ? a));
- unfold;
- intro;
- apply (or_transitive ? ? O');
- [2: apply H
- | skip
- | apply (sup_upper_bound ? ? ? (sup_is_sup ? b))
- ].
-qed.
-
-interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
-
-lemma reduce_bas_seq:
- ∀O:ordered_set.∀a:nat→O.∀p.∀i.
- bas_seq ? (mk_bounded_above_sequence ? a p) i = a i.
- intros;
- reflexivity.
-qed.
-
-(*lemma reduce_bbs_seq:
- ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
- bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i.
- intros;
- reflexivity.
-qed.*)
-
-axiom inf_extensional:
- ∀O:dedekind_sigma_complete_ordered_set.
- ∀a,b:bounded_below_sequence O.
- (∀i.a i = b i) → inf ? a = inf O b.
-
-lemma eq_to_le: ∀O:ordered_set.∀x,y:O.x=y → x ≤ y.
- intros;
- rewrite > H;
- apply (or_reflexive ? ? O).
-qed.
-
-theorem fatou:
- ∀O':dedekind_sigma_complete_ordered_set.
- ∀f:O'→O'. ∀H:is_order_continuous ? f.
- ∀a:bounded_sequence O'.
- let pb := ? in
- let pa := ? in
- f (liminf ? a) ≤ liminf ? (mk_bounded_sequence ? (λi. f (a i)) pb pa).
- [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? a);
- apply mk_is_bounded_above;
- [2: apply (ioc_is_upper_bound_f_sup ? ? H bas)
- | skip
- ]
- | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? a);
- apply mk_is_bounded_below;
- [2: apply (ioc_is_lower_bound_f_inf ? ? H bbs)
- | skip
- ]
- | intros;
- rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? % ?);
- [ unfold liminf;
- apply le_to_le_sup_sup;
- intro;
- rewrite > reduce_bas_seq;
- rewrite > reduce_bas_seq;
- apply (or_transitive ? ? O');
- [2: apply le_f_inf_inf_f;
- assumption
- | skip
- | apply eq_to_le;
- apply inf_extensional;
- intro;
- reflexivity
- ]
- | assumption
- ]
- ].
-qed.
-
-record cotransitively_ordered_set: Type :=
- { cos_ordered_set :> ordered_set;
- cos_cotransitive: cotransitive ? (os_le cos_ordered_set)
- }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/sets/".
-
-include "nat/nat.ma".
-
-definition set ≝ λX:Type.X → Prop.
-
-definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
-
-notation "hvbox(x break ∈ A)" with precedence 60
-for @{ 'member_of $x $A }.
-
-interpretation "Member of" 'member_of x A =
- (cic:/matita/sets/member_of.con _ A x).
-
-notation "hvbox(x break ∉ A)" with precedence 60
-for @{ 'not_member_of $x $A }.
-
-interpretation "Not member of" 'not_member_of x A =
- (cic:/matita/logic/connectives/Not.con
- (cic:/matita/sets/member_of.con _ A x)).
-
-definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False.
-
-notation "∅︀" with precedence 100 for @{ 'emptyset }.
-
-interpretation "Emptyset" 'emptyset =
- (cic:/matita/sets/emptyset.con _).
-
-definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
-
-notation "hvbox(A break ⊆ B)" with precedence 60
-for @{ 'subset $A $B }.
-
-interpretation "Subset" 'subset A B =
- (cic:/matita/sets/subset.con _ A B).
-
-definition intersection: ∀X. set X → set X → set X ≝
- λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
-
-notation "hvbox(A break ∩ B)" with precedence 70
-for @{ 'intersection $A $B }.
-
-interpretation "Intersection" 'intersection A B =
- (cic:/matita/sets/intersection.con _ A B).
-
-definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
-
-notation "hvbox(A break ∪ B)" with precedence 65
-for @{ 'union $A $B }.
-
-interpretation "Union" 'union A B =
- (cic:/matita/sets/union.con _ A B).
-
-definition seq ≝ λX:Type.nat → X.
-
-definition nth ≝ λX.λA:seq X.λi.A i.
-
-notation "hvbox(A \sub i)" with precedence 100
-for @{ 'nth $A $i }.
-
-interpretation "nth" 'nth A i =
- (cic:/matita/sets/nth.con _ A i).
-
-definition countable_union: ∀X. seq (set X) → set X ≝
- λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
-
-notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
-for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
-
-interpretation "countable_union" 'big_union η.t =
- (cic:/matita/sets/countable_union.con _ t).
-
-definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
-
-notation "A \sup 'c'" with precedence 100
-for @{ 'complement $A }.
-
-interpretation "Complement" 'complement A =
- (cic:/matita/sets/complement.con _ A).
-
-definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
- λX,Y,f,B,x. f x ∈ B.
-
-notation "hvbox(f \sup (-1))" with precedence 100
-for @{ 'finverse $f }.
-
-interpretation "Inverse image" 'finverse f =
- (cic:/matita/sets/inverse_image.con _ _ f).
\ No newline at end of file
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/sigma_algebra/".
-
-include "topology.ma".
-
-record is_sigma_algebra (X:Type) (A: set X) (M: set (set X)) : Prop ≝
- { siga_subset: ∀B.B ∈ M → B ⊆ A;
- siga_full: A ∈ M;
- siga_compl: ∀B.B ∈ M → B \sup c ∈ M;
- siga_enumerable_union:
- ∀B:seq (set X).(∀i.(B \sub i) ∈ M) → (∪ \sub i B \sub i) ∈ M
- }.
-
-record sigma_algebra : Type ≝
- { siga_carrier:> Type;
- siga_domain:> set siga_carrier;
- M: set (set siga_carrier);
- siga_is_sigma_algebra:> is_sigma_algebra ? siga_domain M
- }.
-
-(*definition is_measurable_map ≝
- λX:sigma_algebra.λY:topological_space.λf:X → Y.
- ∀V. V ∈ O Y → f \sup -1 V ∈ M X.*)
-definition is_measurable_map ≝
- λX:sigma_algebra.λY:topological_space.λf:X → Y.
- ∀V. V ∈ O Y → inverse_image ? ? f V ∈ M X.
-
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/topology/".
-
-include "sets.ma".
-
-record is_topology (X) (A: set X) (O: set (set X)) : Prop ≝
- { top_subset: ∀B. B ∈ O → B ⊆ A;
- top_empty: ∅︀ ∈ O;
- top_full: A ∈ O;
- top_intersection: ∀B,C. B ∈ O → C ∈ O → B ∩ C ∈ O;
- top_countable_union:
- ∀B.(∀i.(B \sub i) ∈ O) → (∪ \sub i (B \sub i)) ∈ O
- }.
-
-record topological_space : Type ≝
- { top_carrier:> Type;
- top_domain:> set top_carrier;
- O: set (set top_carrier);
- top_is_topological_space:> is_topology ? top_domain O
- }.
-
-(*definition is_continuous_map ≝
- λX,Y: topological_space.λf: X → Y.
- ∀V. V ∈ O Y → (f \sup -1) V ∈ O X.*)
-definition is_continuous_map ≝
- λX,Y: topological_space.λf: X → Y.
- ∀V. V ∈ O Y → inverse_image ? ? f V ∈ O X.
-
-record continuous_map (X,Y: topological_space) : Type ≝
- { cm_f:> X → Y;
- cm_is_continuous_map: is_continuous_map ? ? cm_f
- }.
\ No newline at end of file
projects / helm.git / commitdiff