Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### On the Characterization of Hausdorff Spaces

**by****Artur Kornilowicz**- Received April 18, 1998
- MML identifier: YELLOW12

- [ Mizar article, MML identifier index ]

environ vocabulary TARSKI, RELAT_1, PARTFUN1, FUNCT_3, BOOLE, FUNCT_1, WAYBEL_0, ORDERS_1, LATTICES, YELLOW_0, LATTICE3, ORDINAL2, RELAT_2, WAYBEL_3, WAYBEL_2, QUANTAL1, WELLORD1, WAYBEL11, BHSP_3, SETFAM_1, PRE_TOPC, CANTOR_1, SUBSET_1, CONNSP_2, TOPS_1, TOPS_2, T_0TOPSP, YELLOW_6, YELLOW_9, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, MCART_1, FUNCT_3, PRE_TOPC, TOPS_1, TOPS_2, CANTOR_1, CONNSP_2, BORSUK_1, T_0TOPSP, WELLORD1, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL11, YELLOW_9; constructors TOPS_1, TOPS_2, T_0TOPSP, BORSUK_2, CANTOR_1, YELLOW_4, WAYBEL_1, WAYBEL_3, WAYBEL11, TOLER_1, ORDERS_3, YELLOW_8, YELLOW_9, XCMPLX_0, MEMBERED; clusters STRUCT_0, PRE_TOPC, BORSUK_1, RELSET_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_9, SUBSET_1, XREAL_0, MEMBERED, ZFMISC_1; requirements SUBSET, BOOLE; begin :: The properties of some functions reserve A, B, X, Y for set; definition let X be empty set; cluster union X -> empty; end; theorem :: YELLOW12:1 (delta X).:A c= [:A,A:]; theorem :: YELLOW12:2 (delta X)"[:A,A:] c= A; theorem :: YELLOW12:3 for A being Subset of X holds (delta X)"[:A,A:] = A; theorem :: YELLOW12:4 dom <:pr2(X,Y),pr1(X,Y):> = [:X,Y:] & rng <:pr2(X,Y),pr1(X,Y):> = [:Y,X:]; theorem :: YELLOW12:5 <:pr2(X,Y),pr1(X,Y):>.:[:A,B:] c= [:B,A:]; theorem :: YELLOW12:6 for A being Subset of X, B being Subset of Y holds <:pr2(X,Y),pr1(X,Y):>.:[:A,B:] = [:B,A:]; theorem :: YELLOW12:7 <:pr2(X,Y),pr1(X,Y):> is one-to-one; definition let X, Y be set; cluster <:pr2(X,Y),pr1(X,Y):> -> one-to-one; end; theorem :: YELLOW12:8 <:pr2(X,Y),pr1(X,Y):>" = <:pr2(Y,X),pr1(Y,X):>; begin :: The properties of the relational structures theorem :: YELLOW12:9 for L1 being Semilattice, L2 being non empty RelStr for x, y being Element of L1, x1, y1 being Element of L2 st the RelStr of L1 = the RelStr of L2 & x = x1 & y = y1 holds x "/\" y = x1 "/\" y1; theorem :: YELLOW12:10 for L1 being sup-Semilattice, L2 being non empty RelStr for x, y being Element of L1, x1, y1 being Element of L2 st the RelStr of L1 = the RelStr of L2 & x = x1 & y = y1 holds x "\/" y = x1 "\/" y1; theorem :: YELLOW12:11 for L1 being Semilattice, L2 being non empty RelStr for X, Y being Subset of L1, X1, Y1 being Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = X1 & Y = Y1 holds X "/\" Y = X1 "/\" Y1; theorem :: YELLOW12:12 for L1 being sup-Semilattice, L2 being non empty RelStr for X, Y being Subset of L1, X1, Y1 being Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = X1 & Y = Y1 holds X "\/" Y = X1 "\/" Y1; theorem :: YELLOW12:13 for L1 being antisymmetric up-complete (non empty reflexive RelStr), L2 being non empty reflexive RelStr, x being Element of L1, y being Element of L2 st the RelStr of L1 = the RelStr of L2 & x = y holds waybelow x = waybelow y & wayabove x = wayabove y; theorem :: YELLOW12:14 for L1 being meet-continuous Semilattice, L2 being non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 holds L2 is meet-continuous; theorem :: YELLOW12:15 for L1 being continuous antisymmetric (non empty reflexive RelStr), L2 being non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 holds L2 is continuous; theorem :: YELLOW12:16 for L1, L2 being RelStr, A being Subset of L1, J being Subset of L2 st the RelStr of L1 = the RelStr of L2 & A = J holds subrelstr A = subrelstr J; theorem :: YELLOW12:17 for L1, L2 being non empty RelStr, A being SubRelStr of L1, J being SubRelStr of L2 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the RelStr of J & A is meet-inheriting holds J is meet-inheriting; theorem :: YELLOW12:18 for L1, L2 being non empty RelStr, A being SubRelStr of L1, J being SubRelStr of L2 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the RelStr of J & A is join-inheriting holds J is join-inheriting; theorem :: YELLOW12:19 for L1 being up-complete antisymmetric (non empty reflexive RelStr), L2 being non empty reflexive RelStr, X being Subset of L1, Y being Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = Y & X has_the_property_(S) holds Y has_the_property_(S); theorem :: YELLOW12:20 for L1 being up-complete antisymmetric (non empty reflexive RelStr), L2 being non empty reflexive RelStr, X being Subset of L1, Y being Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = Y & X is directly_closed holds Y is directly_closed; theorem :: YELLOW12:21 for N being antisymmetric with_infima RelStr, D, E being Subset of N for X being upper Subset of N st D misses X holds D "/\" E misses X; theorem :: YELLOW12:22 for R being reflexive non empty RelStr holds id the carrier of R c= (the InternalRel of R) /\ the InternalRel of (R~); theorem :: YELLOW12:23 for R being antisymmetric RelStr holds (the InternalRel of R) /\ the InternalRel of (R~) c= id the carrier of R; theorem :: YELLOW12:24 for R being upper-bounded Semilattice, X being Subset of [:R,R:] st ex_inf_of (inf_op R).:X,R holds inf_op R preserves_inf_of X; definition let R be complete Semilattice; cluster inf_op R -> infs-preserving; end; theorem :: YELLOW12:25 for R being lower-bounded sup-Semilattice, X being Subset of [:R,R:] st ex_sup_of (sup_op R).:X,R holds sup_op R preserves_sup_of X; definition let R be complete sup-Semilattice; cluster sup_op R -> sups-preserving; end; theorem :: YELLOW12:26 for N being Semilattice, A being Subset of N st subrelstr A is meet-inheriting holds A is filtered; theorem :: YELLOW12:27 for N being sup-Semilattice, A being Subset of N st subrelstr A is join-inheriting holds A is directed; theorem :: YELLOW12:28 for N being transitive RelStr, A, J being Subset of N st A is_coarser_than uparrow J holds uparrow A c= uparrow J; theorem :: YELLOW12:29 for N being transitive RelStr, A, J being Subset of N st A is_finer_than downarrow J holds downarrow A c= downarrow J; theorem :: YELLOW12:30 for N being non empty reflexive RelStr for x being Element of N, X being Subset of N st x in X holds uparrow x c= uparrow X; theorem :: YELLOW12:31 for N being non empty reflexive RelStr for x being Element of N, X being Subset of N st x in X holds downarrow x c= downarrow X; begin :: On the Hausdorff Spaces reserve R, S, T for non empty TopSpace; definition let T be non empty TopStruct; cluster the TopStruct of T -> non empty; end; definition let T be TopSpace; cluster the TopStruct of T -> TopSpace-like; end; theorem :: YELLOW12:32 for S, T being TopStruct, B being Basis of S st the TopStruct of S = the TopStruct of T holds B is Basis of T; theorem :: YELLOW12:33 for S, T being TopStruct, B being prebasis of S st the TopStruct of S = the TopStruct of T holds B is prebasis of T; theorem :: YELLOW12:34 for J being Basis of T holds J is non empty; definition let T be non empty TopSpace; cluster -> non empty Basis of T; end; theorem :: YELLOW12:35 for x being Point of T, J being Basis of x holds J is non empty; definition let T be non empty TopSpace, x be Point of T; cluster -> non empty Basis of x; end; theorem :: YELLOW12:36 for S1, T1, S2, T2 being non empty TopSpace, f being map of S1, S2, g being map of T1, T2 st the TopStruct of S1 = the TopStruct of T1 & the TopStruct of S2 = the TopStruct of T2 & f = g & f is continuous holds g is continuous; theorem :: YELLOW12:37 id the carrier of T = {p where p is Point of [:T,T:]: pr1(the carrier of T,the carrier of T).p = pr2(the carrier of T,the carrier of T).p}; theorem :: YELLOW12:38 delta the carrier of T is continuous map of T, [:T,T:]; theorem :: YELLOW12:39 pr1(the carrier of S,the carrier of T) is continuous map of [:S,T:], S; theorem :: YELLOW12:40 pr2(the carrier of S,the carrier of T) is continuous map of [:S,T:], T; theorem :: YELLOW12:41 for f being continuous map of T, S, g being continuous map of T, R holds <:f,g:> is continuous map of T, [:S,R:]; theorem :: YELLOW12:42 <:pr2(the carrier of S,the carrier of T), pr1(the carrier of S,the carrier of T):> is continuous map of [:S,T:],[:T,S:]; theorem :: YELLOW12:43 for f being map of [:S,T:], [:T,S:] st f = <:pr2(the carrier of S,the carrier of T), pr1(the carrier of S,the carrier of T):> holds f is_homeomorphism; theorem :: YELLOW12:44 [:S,T:], [:T,S:] are_homeomorphic; theorem :: YELLOW12:45 for T being Hausdorff (non empty TopSpace) for f, g being continuous map of S, T holds (for X being Subset of S st X = {p where p is Point of S: f.p <> g.p} holds X is open) & for X being Subset of S st X = {p where p is Point of S: f.p = g.p} holds X is closed; theorem :: YELLOW12:46 T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed; definition let S, T be TopStruct; cluster strict Refinement of S, T; end; definition let S be non empty TopStruct, T be TopStruct; cluster strict non empty Refinement of S, T; cluster strict non empty Refinement of T, S; end; theorem :: YELLOW12:47 for R, S, T being TopStruct holds R is Refinement of S, T iff the TopStruct of R is Refinement of S, T; reserve S1, S2, T1, T2 for non empty TopSpace, R for Refinement of [:S1,T1:], [:S2,T2:], R1 for Refinement of S1, S2, R2 for Refinement of T1, T2; theorem :: YELLOW12:48 the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies { [:U1,V1:] /\ [:U2,V2:] where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : U1 is open & U2 is open & V1 is open & V2 is open } is Basis of R; theorem :: YELLOW12:49 the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R; theorem :: YELLOW12:50 the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies [:R1,R2:] is Refinement of [:S1,T1:], [:S2,T2:];

Back to top