|
prelude_sets_aux[T:TYPE]: THEORY
BEGIN
x: VAR T
A: VAR setofsets[T]
a,b: VAR set[T]
F: VAR finite_set[set[T]]
P: VAR [set[T]->bool]
complement_difference: LEMMA
complement(difference(a,b)) = union(complement(a),b)
Intersection_member:
LEMMA member(x,Intersection(A)) IFF (FORALL (a:(A)): member(x,a))
Intersection_split: LEMMA nonempty?(A) IMPLIES
(Intersection(A) = intersection(choose(A),Intersection(rest(A))))
Intersection_finite: LEMMA
P(fullset[T]) AND is_finite(A) AND (FORALL (a:(A)): P(a)) AND
(FORALL (a,b:set[T]): P(a) AND P(b) IMPLIES P(intersection(a,b)))
IMPLIES P(Intersection(A))
Union_member: LEMMA member(x,Union(A)) IFF (EXISTS (a:(A)): member(x,a))
Union_split: LEMMA nonempty?(A) IMPLIES
(Union(A) = union(choose(A),Union(rest(A))))
Union_finite: LEMMA
P(emptyset[T]) AND is_finite(A) AND (FORALL (a:(A)): P(a)) AND
(FORALL (a,b:set[T]): P(a) AND P(b) IMPLIES P(union(a,b)))
IMPLIES P(Union(A))
finite_Complement: LEMMA is_finite(Complement(F))
%------------------------------------------------------------------------
% A Transition From An Epsilon Delta Property To The Existence
% Of A Particular (Helpful Sequence). This May Be Helpful In Proving
% Certain Properties Related To Continuity And/Or Metric Space.
%
% Anthony Narkawicz
%
%------------------------------------------------------------------------
S: VAR set[T]
f: VAR [T -> posreal]
epsilon_to_sequence: LEMMA
(FORALL (epsilon: posreal): EXISTS (s: (S)):
f(s) < epsilon)IMPLIES
(EXISTS (seq: [posint -> (S)]): FORALL (n: posint): f(seq(n)) < 1/n)
END prelude_sets_aux
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
