% problem-set/topology/point.set/lemma1d.clauses % created : 08/08/88 % revised : 08/17/89 % description : % % lemma 1d: If xb is a basis for x, then for any subset u of the topology % generated by xb, sigma(u) is also in the topology. % representation : % % See axioms.decl for a full explanation. % top_space definition: -top_space(x,xt) | el_s(0,xt). -top_space(x,xt) | el_s(x,xt). -top_space(x,xt) | -el_s(y,xt) | -el_s(w,xt) | el_s(inter_s(y,w),xt). -top_space(x,xt) | -subset_s(z,xt) | el_s(sigma(z),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | subset_s(f3(x,xt),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | -el_s(sigma(f3(x,xt)),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | subset_s(f3(x,xt),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | -el_s(sigma(f3(x,xt)),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | -el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | subset_s(f3(x,xt),xt). top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | -el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | -el_s(sigma(f3(x,xt)),xt). % topology definition: -topology(xt) | top_space(f4(xt),xt). topology(xt) | -top_space(uu4,xt). eq_s(f4(xt),sigma(xt)). % open set definition: -open(u,x,xt) | top_space(x,xt). -open(u,x,xt) | el_s(u,xt). open(u,x,xt) | -top_space(x,xt) | -el_s(u,xt). % basis for a topology definition: -basis(xb,x) | eq_s(sigma(xb),x). -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | el_p(f5(xb,x,xx,xb1,xb2),xb). -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | el_p(xx,f5(xb,x,xx,xb1,xb2)). -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | subset_s(f5(xb,x,xx,xb1,xb2),inter_s(xb1,xb2)). basis(xb,x) | -eq_s(sigma(xb),x) | el_p(f6(xb,x),x). basis(xb,x) | -eq_s(sigma(xb),x) | el_s(f7(xb,x),xb). basis(xb,x) | -eq_s(sigma(xb),x) | el_s(f8(xb,x),xb). basis(xb,x) | -eq_s(sigma(xb),x) | el_p(f6(xb,x),inter_s(f7(xb,x),f8(xb,x))). basis(xb,x) | -eq_s(sigma(xb),x) | -el_p(uu8,xb) | -el_p(f6(xb,x),uu8) | -subset_s(uu8,inter_s(f7(xb,x),f8(xb,x))). % topology generated by a basis definition: -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_s(f9(xb,u,x),xb). -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_p(x,f9(xb,u,x)). -el_s(u,top_of_basis(xb)) | -el_p(x,u) | subset_s(f9(xb,u,x),u). el_s(u,top_of_basis(xb)) | el_p(f10(xb,u),u). el_s(u,top_of_basis(xb)) | -el_s(uu10,xb) | -el_p(f10(xb,u),uu10) | -subset_s(uu10,u). % set theory axioms & lemmas. subset_s(0,x). -el_s(x,0). -el_p(x,0). subset_s(x,x). subset_c(x,x). -subset_s(x,y) | -subset_s(y,z) | subset_s(x,z). -subset_c(x,y) | -subset_c(y,z) | subset_c(x,z). -el_p(z,sigma(x)) | el_s(g1(z,x),x). -el_p(z,sigma(x)) | el_p(z,g1(z,x)). el_p(z,sigma(x)) | -el_s(uu1,x) | -el_p(z,uu1). -el_s(x,y) | subset_s(x,sigma(y)). -subset_s(x,y) | -el_s(y,z) | subset_s(x,sigma(z)). -subset_s(x,y) | -el_p(u,x) | el_p(u,y). subset_s(x,y) | el_p(g3(x,y),x). subset_s(x,y) | -el_p(g3(x,y),y). -subset_c(x,y) | -el_s(u,x) | el_s(u,y). subset_c(x,y) | el_s(g4(x,y),x). subset_c(x,y) | -el_s(g4(x,y),y). -el_p(z,inter_s(x,y)) | el_p(z,x). -el_p(z,inter_s(x,y)) | el_p(z,y). el_p(z,inter_s(x,y)) | -el_p(z,x) | -el_p(z,y). -el_s(z,join_c(x,y)) | el_s(z,x) | el_s(z,y). el_s(z,join_c(x,y)) | -el_s(z,x). el_s(z,join_c(x,y)) | -el_s(z,y). -el_p(z,join_s(x,y)) | el_p(z,x) | el_p(z,y). el_p(z,join_s(x,y)) | -el_p(z,x). el_p(z,join_s(x,y)) | -el_p(z,y). -subset_s(x1,y1) | -subset_s(x2,y2) | subset_s(inter_s(x1,x2),inter_s(y1,y2)). % equality axioms: eq_s(x,x). eq_c(x,x). eq_p(x,x). -eq_s(x,y) | eq_s(y,x). eq_s(x,y) | -eq_s(y,x). -eq_s(x,y) | -eq_s(y,z) | eq_s(x,z). -eq_c(x,y) | eq_c(y,x). eq_c(x,y) | -eq_c(y,x). -eq_c(x,y) | -eq_c(y,z) | eq_c(x,z). -eq_p(x,y) | eq_p(y,x). eq_p(x,y) | -eq_p(y,x). -eq_p(x,y) | -eq_p(y,z) | eq_p(x,z). % equality substitution axioms: -eq_c(x,y) | -subset_c(x,z) | subset_c(y,z). -eq_s(x,y) | -subset_s(z,x) | subset_s(z,y). -eq_s(x,y) | -top_space(x,z) | top_space(y,z). -eq_c(x,y) | -top_space(z,x) | top_space(z,y). -eq_c(x,y) | -topology(x) | topology(y). -eq_s(x,y) | -el_s(x,z) | el_s(y,z). -eq_s(x,y) | -el_p(z,x) | el_p(z,y). -eq_c(x,y) | -el_s(z,x) | el_s(z,y). -eq_s(x,y) | -open(x,z,w) | open(y,z,w). -eq_s(x,y) | -open(z,x,w) | open(z,y,w). -eq_c(x,y) | -open(w,z,x) | open(w,z,y). -eq_c(x,y) | -basis(x,z) | basis(y,z). -eq_s(x,y) | -basis(z,x) | basis(z,y). -eq_s(x,y) | eq_s(inter_s(x,z),inter_s(y,z)). eq_s(inter_s(x,y),inter_s(y,x)). -eq_c(x,y) | eq_s(sigma(x),sigma(y)). -eq_c(x,y) | eq_c(top_of_basis(x),top_of_basis(y)). % equality predicates: -eq_s(x,y) | subset_s(x,y). -eq_s(x,y) | subset_s(y,x). eq_s(x,y) | -subset_s(x,y) | -subset_s(y,x). -eq_c(x,y) | subset_c(x,y). -eq_c(x,y) | subset_c(y,x). eq_c(x,y) | -subset_c(x,y) | -subset_c(y,x). % denial: subset_c(U,top_of_basis(B)). -el_s(sigma(U),top_of_basis(B)). eq_s(f4(xt),sigma(xt)). eq_s(inter_s(x,y),inter_s(y,x)). eq_c(inter_c(x,y),inter_c(y,x)). eq_s(join_s(x,y),join_s(y,x)). eq_c(join_c(x,y),join_c(y,x)). eq_s(inter_s(inter_s(x,y),z), inter_s(x,inter_s(y,z))). eq_c(inter_c(inter_c(x,y),z), inter_c(x,inter_c(y,z))). eq_s(join_s(join_s(x,y),z), join_s(x,join_s(y,z))). eq_c(join_c(join_c(x,y),z), join_c(x,join_c(y,z))). eq_s(inter_s(x,x),x). eq_s(inter_s(x,0),0). eq_s(inter_s(0,x),0). eq_s(join_s(x,x),x). eq_s(join_s(x,0),x). eq_s(join_s(0,x),x). eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)). eq_c(inter_c(x,inter_c(x,y)),inter_c(x,y)). eq_s(inter_s(x,inter_s(y,x)),inter_s(x,y)). eq_c(inter_c(x,inter_c(y,x)),inter_c(x,y)). eq_s(join_s(x,join_s(x,y)),join_s(x,y)). eq_c(join_c(x,join_c(x,y)),join_c(x,y)). eq_s(join_s(x,join_s(y,x)),join_s(x,y)). eq_c(join_c(x,join_c(y,x)),join_c(x,y)).