% problem-set/topology/point.set/axioms.decl % created : 08/04/88 % revised : 08/18/89 % description : % % DECLARATIONS FOR TOPOLOGY FILES % representation : % CONSTANTS % 0 : empty set % X : standard space % T : a standard topology on X % B : a standard basis for the topology on X % U : an open subset of X % V : another subset of X, variously an open one or the complement of U % PREDICATES % subset_s(x,y) : x is a subset of y % x and y must be sets % subset_c(x,y) : x is a subset of y % x and y must be collections % eq_s(x,y) : usual equality of sets, except that for sets equality is % actually subset_s(x,y) & subset_s(y,x) % eq_c(x,y) : usual equality of collections, except that for collections % equality is actually subset_c(x,y) & subset_c(y,x) % eq_p(x,y) : usual equality of points % top_space(x,xt) : x is a space with xt the topology on it % x must be a set and xt must be a collection % topology(xt) : xt is a topology; note that the space is sigma(xt) % xt must be a collection % el_s(x,y) : x is an element of y % x must be a set and y must be a collection % el_p(x,y) : x is an element of y % x must be a point and y must be a set % open(u,x,xt) : u is an open subset of space x in topology xt % u and x must be sets, xt must be a collection % closed(u,x,xt) : u is a closed subset of space x in topology xt % u and x must be sets, xt must be a collection % finer(xt,xs,x) : topology xt is finer than topology xs on space x % xt and xs must be collections, x must be a set % basis(xb,x) : collection xb is a basis for a topology on space x % xb must be a collection, x must be a set % subbasis(xs,x) : collection xs is a subbasis for a topology on space x % xs must be a collection, x must be a set % FUNCTIONS % inter_s(u,v) : the intersection of two sets % inter_c(u,v) : the intersection of two collections % join_s(u,v) : the union of two sets % join_c(u,v) : the union of two collections % sigma(z) : the set consisting of the union of the elements of z % z must be a collection % tau(z) : the set consisting of the intersection of the elements of z % z must be a collection % rel_comp(u,x) : the relative complement of u with respect to x % u and x must be sets % top_of_basis(xb) : names the topology generated by the basis xb; % note that the space is given by sigma(xb) % xb must be a collection % basis_of_subbasis(xs) : names the basis generated by the subbasis xs, % the collection of all finite intersections of elements of xs % xs must be a collection % top_of_subbasis(xs) : names the topology generated by the subbasis xs; % note that the space is given by sigma(xs) % xs must be a collection % subspace_top(x,xt,y) : names the topology on the subspace y of space x % under topology xt % x and y must be sets, xt must be a collection % SKOLEM FUNCTIONS % From Topology Definitions % f1(x,xt) : in the definition of top_space, names a subcollection of the % topology xt such that inter_s(f1,f2) is not a member of xt % x must be a set and xt must be a collection % f2(x,xt) : in the definition of top_space, names a subcollection of the % topology xt such that inter_s(f1,f2) is not a member of xt % x must be a set and xt must be a collection % f3(x,xt) : in the definition of top_space, names a subcollection of the % topology xt such that sigma(f3(x,xt)) is not a member of xt % x must be a set and xt must be a collection % f4(xt) : in the definition of topology, names the space for which xt % is a topology, namely sigma(xt) % xt must be a collection % f5(xb,x,xx,xb1,xb2) : in the definition of basis, names the basis % element lying in the intersection of the two previously-given % basis elements % xb, xb1, and xb2 must be collections, x must be a set, and % xx must be a point % f6(xb,x) : in the definition of basis, names a point in x % xb must be a collection and x must be a set % f7(xb,x) : in the definition of basis, names a first basis element % xb must be a collection and x must be a set % f8(xb,x) : in the definition of basis, names a second basis element % xb must be a collection and x must be a set % f9(xb,u,x) : in the definition of top_of_basis, names an element of the % basis which is a neighborhood of a point contained in set u % xb must be a collection, u must be a set, x must be a point % f10(xb,u) : in the definition of top_of_basis, names a point in u which % has no basis element containing it contained in u % xb must be a collection and u must be a set % f11(x,xt,y,u) : in the definition of subspace_top, names the element of % the topology xt for which intersect(f11(x,xt,y,u),y)=u % x, y, and u must be sets, xt must be a collection % From Set Theory % g1(z,x) : in the definition of sigma, names the element of sigma(x) which % has z as an element % z must be a point, x must be a collection % g2(z,x) : in the definition of tau, names an element of the collection x % which does not contain point z % z must be a point, x must be a collection % g3(x,y) : in the definition of subset_s, names a point in x which is not in y % x and y must be sets % g4(x,y) : in the definition of subset_c, names a set which is an element % of x which is not an element of y % x and y must be sets