Quelle  prelude_sets_aux.pvs

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