|
convergence_set[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% Convergence properties for uncountable sets
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 20/4/05
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING countable_convergence[T]
a: VAR real
nz: VAR nzreal
X,Y: VAR set[T]
t: VAR T
f,g: VAR [T -> real]
nonzero_elts(f,X):set[T] = {t | X(t) AND f(t) /= 0}
convergent?(X)(f): bool
= is_countable(nonzero_elts(f,X)) AND convergent?(nonzero_elts(f,X))(f)
convergent_zero: LEMMA convergent?(X)(LAMBDA t: 0)
convergent_plus: LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
convergent?(X)(f+g)
convergent_scal: LEMMA convergent?(X)(f) => convergent?(X)(a*f)
convergent_opp: LEMMA convergent?(X)(f) => convergent?(X)(-f)
convergent_diff: LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
convergent?(X)(f-g)
convergent_le: LEMMA (FORALL t: abs(g(t)) <= abs(f(t))) AND
convergent?(X)(f) => convergent?(X)(g)
convergent_empty: LEMMA convergent?(emptyset[T])(g)
convergent_singleton: LEMMA convergent?(singleton(t))(g)
convergent_subset: LEMMA subset?(X,Y) AND convergent?(Y)(g) =>
convergent?(X)(g)
convergent_intersection: LEMMA
convergent?(X)(g) OR convergent?(Y)(g) => convergent?(intersection(X,Y))(g)
convergent_difference: LEMMA
convergent?(X)(g) => convergent?(difference(X,Y))(g)
convergent_disjoint_union: LEMMA
disjoint?(X,Y) AND convergent?(X)(g) AND convergent?(Y)(g) =>
convergent?(union(X,Y))(g)
convergent_union: LEMMA
convergent?(X)(g) AND convergent?(Y)(g) => convergent?(union(X,Y))(g)
convergent_add: LEMMA convergent?(X)(g) =>
convergence_set.convergent?(add(t,X))(g)
convergent_remove: LEMMA convergent?(X)(g) => convergent?(remove(t,X))(g)
convergent_abs: LEMMA convergent?(X)(g) IFF convergent?(X)(abs(g))
END convergence_set
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
