### The Mizar article:

### On Kolmogorov Topological Spaces

**by****Zbigniew Karno**

- Received July 26, 1994
Copyright (c) 1994 Association of Mizar Users

- MML identifier: TSP_1
- [ MML identifier index ]

environ vocabulary PRE_TOPC, BOOLE, SUBSET_1, METRIC_1, REALSET1, TDLAT_3, NATTRA_1, SETFAM_1, TARSKI, COLLSP, TSP_1; notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, BORSUK_1, TSEP_1, TDLAT_3, TEX_1, TEX_2, T_0TOPSP, TEX_4; constructors REALSET1, TSEP_1, TDLAT_3, TEX_2, T_0TOPSP, TEX_4, BORSUK_1, MEMBERED; clusters TDLAT_3, TEX_1, TEX_2, STRUCT_0, MEMBERED, ZFMISC_1; requirements SUBSET, BOOLE; definitions T_0TOPSP; theorems ZFMISC_1, REALSET1, SUBSET_1, PRE_TOPC, TOPS_1, PCOMPS_1, TSEP_1, TDLAT_3, TEX_1, TEX_2, TEX_4, TARSKI, T_0TOPSP, STRUCT_0, XBOOLE_0, XBOOLE_1; begin :: 1. Subspaces. definition let Y be TopStruct; redefine mode SubSpace of Y -> TopStruct means :Def1: the carrier of it c= the carrier of Y & for G0 being Subset of it holds G0 is open iff ex G being Subset of Y st G is open & G0 = G /\ the carrier of it; compatibility proof let Y0 be TopStruct; A1: [#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y by PRE_TOPC:12; thus Y0 is SubSpace of Y implies the carrier of Y0 c= the carrier of Y & for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of Y st G is open & G0 = G /\ the carrier of Y0 proof assume A2: Y0 is SubSpace of Y; hence the carrier of Y0 c= the carrier of Y by A1,PRE_TOPC:def 9; thus for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of Y st G is open & G0 = G /\ the carrier of Y0 proof let G0 be Subset of Y0; thus G0 is open implies ex G being Subset of Y st G is open & G0 = G /\ the carrier of Y0 proof assume G0 is open; then G0 in the topology of Y0 by PRE_TOPC:def 5; then consider G being Subset of Y such that A3: G in the topology of Y and A4: G0 = G /\ [#] Y0 by A2,PRE_TOPC:def 9 ; reconsider G as Subset of Y; take G; thus G is open by A3,PRE_TOPC:def 5; thus G0 = G /\ the carrier of Y0 by A4,PRE_TOPC:12; end; given G being Subset of Y such that A5: G is open and A6: G0 = G /\ the carrier of Y0; now take G; thus G in the topology of Y by A5,PRE_TOPC:def 5; thus G0 = G /\ [#]Y0 by A6,PRE_TOPC:12; end; then G0 in the topology of Y0 by A2,PRE_TOPC:def 9; hence G0 is open by PRE_TOPC:def 5; end; end; assume A7: the carrier of Y0 c= the carrier of Y & for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of Y st G is open & G0 = G /\ the carrier of Y0; now thus [#]Y0 c= [#]Y by A1,A7; thus for G0 being Subset of Y0 holds G0 in the topology of Y0 iff ex G being Subset of Y st G in the topology of Y & G0 = G /\ [#]Y0 proof let G0 be Subset of Y0; thus G0 in the topology of Y0 implies ex G being Subset of Y st G in the topology of Y & G0 = G /\ [#]Y0 proof reconsider M = G0 as Subset of Y0; assume G0 in the topology of Y0; then M is open by PRE_TOPC:def 5; then consider G being Subset of Y such that A8: G is open and A9: G0 = G /\ the carrier of Y0 by A7; take G; thus G in the topology of Y by A8,PRE_TOPC:def 5; thus G0 = G /\ [#]Y0 by A9,PRE_TOPC:12; end; given G being Subset of Y such that A10: G in the topology of Y and A11: G0 = G /\ [#]Y0; reconsider G as Subset of Y; reconsider M = G0 as Subset of Y0; now take G; thus G is open by A10,PRE_TOPC:def 5; thus G0 = G /\ the carrier of Y0 by A11,PRE_TOPC:12; end; then M is open by A7; hence G0 in the topology of Y0 by PRE_TOPC:def 5; end; end; hence Y0 is SubSpace of Y by PRE_TOPC:def 9; end; coherence; end; canceled; theorem Th2: for Y being TopStruct, Y0 being SubSpace of Y for G being Subset of Y st G is open holds ex G0 being Subset of Y0 st G0 is open & G0 = G /\ the carrier of Y0 proof let Y be TopStruct, Y0 be SubSpace of Y; [#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y by PRE_TOPC:12; then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def 9; let G be Subset of Y; G /\ A is Subset of Y0 by XBOOLE_1:17; then reconsider G0 = G /\ A as Subset of Y0; assume A1: G is open; take G0; thus G0 is open by A1,Def1; thus G0 = G /\ the carrier of Y0; end; definition let Y be TopStruct; redefine mode SubSpace of Y -> TopStruct means :Def2: the carrier of it c= the carrier of Y & for F0 being Subset of it holds F0 is closed iff ex F being Subset of Y st F is closed & F0 = F /\ the carrier of it; compatibility proof let Y0 be TopStruct; A1: [#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y by PRE_TOPC:12; thus Y0 is SubSpace of Y implies the carrier of Y0 c= the carrier of Y & for F0 being Subset of Y0 holds F0 is closed iff ex F being Subset of Y st F is closed & F0 = F /\ the carrier of Y0 proof assume A2: Y0 is SubSpace of Y; then A3: [#]Y0 c= [#]Y by PRE_TOPC:def 9; thus the carrier of Y0 c= the carrier of Y by A1,A2,PRE_TOPC:def 9; A4: [#]Y0 \ [#]Y = {} by A3,XBOOLE_1:37; thus for F0 being Subset of Y0 holds F0 is closed iff ex F being Subset of Y st F is closed & F0 = F /\ the carrier of Y0 proof let F0 be Subset of Y0; thus F0 is closed implies ex F being Subset of Y st F is closed & F0 = F /\ the carrier of Y0 proof assume F0 is closed; then [#]Y0 \ F0 is open by PRE_TOPC:def 6; then consider G being Subset of Y such that A5: G is open and A6: [#]Y0 \ F0 = G /\ the carrier of Y0 by A2,Def1; take F = [#]Y \ G; A7: G = [#]Y \ F by PRE_TOPC:22; hence F is closed by A5,PRE_TOPC:def 6; F0 = [#]Y0 \ (G /\ the carrier of Y0) by A6,PRE_TOPC:22 .= ([#]Y0 \ G) \/ ([#]Y0 \ the carrier of Y0) by XBOOLE_1:54 .= ([#]Y0 \ G) \/ {} by XBOOLE_1:37 .= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ F) by A7,XBOOLE_1:52 .= [#]Y0 /\ F by A4; hence F0 = F /\ the carrier of Y0 by PRE_TOPC:12; end; given F being Subset of Y such that A8: F is closed and A9: F0 = F /\ the carrier of Y0; set G0 = [#]Y0 \F0; now take G = [#]Y \ F; thus G is open by A8,PRE_TOPC:def 6; A10: F = [#]Y \ G by PRE_TOPC:22; G0 = ([#]Y0 \ F) \/ ([#]Y0 \ the carrier of Y0) by A9,XBOOLE_1: 54 .= ([#]Y0 \ F) \/ {} by XBOOLE_1:37 .= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ G) by A10,XBOOLE_1:52 .= [#]Y0 /\ G by A4; hence G0 = G /\ the carrier of Y0 by PRE_TOPC:12; end; then G0 is open by A2,Def1; hence F0 is closed by PRE_TOPC:def 6; end; end; assume A11: the carrier of Y0 c= the carrier of Y & for F0 being Subset of Y0 holds F0 is closed iff ex F being Subset of Y st F is closed & F0 = F /\ the carrier of Y0; now thus the carrier of Y0 c= the carrier of Y by A11; A12: [#]Y0 \ [#]Y = {} by A1,A11,XBOOLE_1:37; thus for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of Y st G is open & G0 = G /\ the carrier of Y0 proof let G0 be Subset of Y0; thus G0 is open implies ex G being Subset of Y st G is open & G0 = G /\ the carrier of Y0 proof set F0 = [#]Y0 \ G0; assume A13: G0 is open; A14: G0 = [#]Y0 \ F0 by PRE_TOPC:22; then F0 is closed by A13,PRE_TOPC:def 6; then consider F being Subset of Y such that A15: F is closed and A16: F0 = F /\ the carrier of Y0 by A11; take G = [#]Y \ F; A17: F = [#]Y \ G by PRE_TOPC:22; thus G is open by A15,PRE_TOPC:def 6; G0 = ([#]Y0 \ F) \/ ([#]Y0 \ the carrier of Y0) by A14,A16, XBOOLE_1:54 .= ([#]Y0 \ F) \/ {} by XBOOLE_1:37 .= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ G) by A17,XBOOLE_1:52 .= [#]Y0 /\ G by A12; hence G0 = G /\ the carrier of Y0 by PRE_TOPC:12; end; given G being Subset of Y such that A18: G is open and A19: G0 = G /\ the carrier of Y0; set F0 = [#]Y0 \ G0; A20: G0 = [#]Y0 \ F0 by PRE_TOPC:22; now take F = [#]Y \ G; A21: G = [#]Y \ F by PRE_TOPC:22; hence F is closed by A18,PRE_TOPC:def 6; F0 = ([#]Y0 \ G) \/ ([#]Y0 \ the carrier of Y0) by A19,XBOOLE_1: 54 .= ([#]Y0 \ G) \/ {} by XBOOLE_1:37 .= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ F) by A21,XBOOLE_1:52 .= [#]Y0 /\ F by A12; hence F0 = F /\ the carrier of Y0 by PRE_TOPC:12; end; then F0 is closed by A11; hence G0 is open by A20,PRE_TOPC:def 6; end; end; hence Y0 is SubSpace of Y by Def1; end; coherence; end; canceled; theorem Th4: for Y being TopStruct, Y0 being SubSpace of Y for F being Subset of Y st F is closed holds ex F0 being Subset of Y0 st F0 is closed & F0 = F /\ the carrier of Y0 proof let Y be TopStruct, Y0 be SubSpace of Y; [#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y by PRE_TOPC:12; then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def 9; let F be Subset of Y; F /\ A is Subset of Y0 by XBOOLE_1:17; then reconsider F0 = F /\ A as Subset of Y0; assume A1: F is closed; take F0; thus F0 is closed by A1,Def2; thus F0 = F /\ the carrier of Y0; end; begin :: 2. Kolmogorov Spaces. definition let T be TopStruct; redefine attr T is discerning means :Def3: T is empty or for x, y being Point of T st x <> y holds (ex V being Subset of T st V is open & x in V & not y in V) or (ex W being Subset of T st W is open & not x in W & y in W); compatibility proof hereby assume A1: T is discerning; assume A2: T is not empty; let x, y be Point of T; assume x <> y; then ex V being Subset of T st V is open & ((x in V & not y in V) or (y in V & not x in V)) by A1,A2,T_0TOPSP:def 7; hence (ex V being Subset of T st V is open & x in V & not y in V) or (ex W being Subset of T st W is open & not x in W & y in W); end; assume A3: T is empty or for x, y being Point of T st x <> y holds (ex V being Subset of T st V is open & x in V & not y in V) or (ex W being Subset of T st W is open & not x in W & y in W); assume A4: T is not empty; let x,y be Point of T; assume x <> y; then (ex V being Subset of T st V is open & x in V & not y in V) or (ex W being Subset of T st W is open & not x in W & y in W) by A3,A4; hence ex V being Subset of T st V is open & ((x in V & not y in V) or (y in V & not x in V)); end; synonym T is T_0; end; definition let Y be TopStruct; redefine attr Y is T_0 means :Def4: Y is empty or for x, y being Point of Y st x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); compatibility proof thus Y is T_0 implies Y is empty or for x, y being Point of Y st x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F) proof assume A1: Y is empty or for x, y being Point of Y st x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); assume A2: Y is not empty; let x, y be Point of Y; A3: the carrier of Y <> {} by A2,STRUCT_0:def 1; assume A4: x <> y; hereby per cases by A1,A2,A4; suppose ex V being Subset of Y st V is open & x in V & not y in V; then consider V being Subset of Y such that A5: V is open and A6: x in V and A7: not y in V; now take F = V`; F = [#]Y \ V by PRE_TOPC:17; then V = [#]Y \ F by PRE_TOPC:22; hence F is closed by A5,PRE_TOPC:def 6; thus not x in F by A6,SUBSET_1:54; thus y in F by A3,A7,SUBSET_1:50; end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); suppose ex W being Subset of Y st W is open & not x in W & y in W; then consider W being Subset of Y such that A8: W is open and A9: not x in W and A10: y in W; now take E = W`; E = [#]Y \ W by PRE_TOPC:17; then W = [#]Y \ E by PRE_TOPC:22; hence E is closed by A8,PRE_TOPC:def 6; thus x in E by A3,A9,SUBSET_1:50; thus not y in E by A10,SUBSET_1:54; end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); end; end; assume A11: Y is empty or for x, y being Point of Y st x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); Y is not empty implies for x, y being Point of Y st x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) proof assume A12: Y is not empty; let x, y be Point of Y; A13: the carrier of Y <> {} by A12,STRUCT_0:def 1; assume A14: x <> y; hereby per cases by A11,A12,A14; suppose ex E being Subset of Y st E is closed & x in E & not y in E; then consider E being Subset of Y such that A15: E is closed and A16: x in E and A17: not y in E; now take W = E`; W = [#]Y \ E by PRE_TOPC:17; hence W is open by A15,PRE_TOPC:def 6; thus not x in W by A16,SUBSET_1:54; thus y in W by A13,A17,SUBSET_1:50; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose ex F being Subset of Y st F is closed & not x in F & y in F; then consider F being Subset of Y such that A18: F is closed and A19: not x in F and A20: y in F; now take V = F`; V = [#]Y \ F by PRE_TOPC:17; hence V is open by A18,PRE_TOPC:def 6; thus x in V by A13,A19,SUBSET_1:50; thus not y in V by A20,SUBSET_1:54; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; end; hence Y is T_0 by Def3; end; end; definition cluster trivial -> T_0 (non empty TopStruct); coherence proof let Y be non empty TopStruct; assume Y is trivial; then consider a being Point of Y such that A1: the carrier of Y = {a} by TEX_1:def 1; now let x, y be Point of Y; A2: x = a & y = a by A1,TARSKI:def 1; assume x <> y; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A2; end; hence thesis by Def3; end; cluster non T_0 -> non trivial (non empty TopStruct); coherence proof let Y be non empty TopStruct; assume A3: Y is non T_0; assume Y is trivial; then consider a being Point of Y such that A4: the carrier of Y = {a} by TEX_1:def 1; now let x, y be Point of Y; A5: x = a & y = a by A4,TARSKI:def 1; assume x <> y; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A5; end; hence contradiction by A3,Def3; end; end; Lm1: for X being anti-discrete non trivial (non empty TopStruct) holds X is non T_0 proof let X be anti-discrete non trivial (non empty TopStruct); now consider x, y being Point of X such that A1: x <> y by REALSET1:def 20; take x, y; thus x <> y by A1; A2:now let V be Subset of X; assume V is open; then A3: V = {} or V = the carrier of X by TDLAT_3:20; assume x in V; hence y in V by A3; end; now let V be Subset of X; assume V is open; then A4: V = {} or V = the carrier of X by TDLAT_3:20; assume y in V; hence x in V by A4; end; hence not (ex V being Subset of X st V is open & x in V & not y in V) & not (ex W being Subset of X st W is open & not x in W & y in W) by A2; end; hence thesis by Def3; end; definition cluster strict T_0 non empty TopSpace; existence proof consider X being trivial strict (non empty TopSpace); take X; thus thesis; end; cluster strict non T_0 non empty TopSpace; existence proof consider X being anti-discrete non trivial strict (non empty TopSpace); take X; thus thesis by Lm1; end; end; definition cluster discrete -> T_0 (non empty TopSpace); coherence proof let Y be non empty TopSpace; assume A1: Y is discrete; now let x, y be Point of Y; assume A2: x <> y; now take V = {x}; thus V is open by A1,TDLAT_3:17; thus x in V by TARSKI:def 1; thus not y in V by A2,TARSKI:def 1; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; hence thesis by Def3; end; cluster non T_0 -> non discrete (non empty TopSpace); coherence proof let Y be non empty TopSpace; assume A3: Y is non T_0; assume A4: Y is discrete; now let x, y be Point of Y; assume A5: x <> y; now take V = {x}; thus V is open by A4,TDLAT_3:17; thus x in V by TARSKI:def 1; thus not y in V by A5,TARSKI:def 1; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; hence contradiction by A3,Def3; end; cluster anti-discrete non trivial -> non T_0 (non empty TopSpace); coherence by Lm1; cluster anti-discrete T_0 -> trivial (non empty TopSpace); coherence by Lm1; cluster T_0 non trivial -> non anti-discrete (non empty TopSpace); coherence by Lm1; end; Lm2: for X being non empty TopSpace, x being Point of X holds x in Cl {x} proof let X be non empty TopSpace, x be Point of X; x in {x} & {x} c= Cl {x} by PRE_TOPC:48,TARSKI:def 1; hence thesis; end; Lm3: for X being non empty TopSpace, A, B being Subset of X holds B c= Cl A implies Cl B c= Cl A proof let X be non empty TopSpace, A, B be Subset of X; assume A1: B c= Cl A; Cl A is closed by PCOMPS_1:4; hence thesis by A1,TOPS_1:31; end; definition let X be non empty TopSpace; redefine attr X is T_0 means :Def5: for x, y being Point of X st x <> y holds Cl {x} <> Cl {y}; compatibility proof thus X is T_0 implies for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} proof assume A1: X is T_0; hereby let x, y be Point of X; assume A2: x <> y; now per cases by A1,A2,Def3; suppose ex V being Subset of X st V is open & x in V & not y in V; then consider V being Subset of X such that A3: V is open and A4: x in V and A5: not y in V; y in V` by A5,SUBSET_1:50; then {y} c= V` by ZFMISC_1:37; then {y} misses V by SUBSET_1:43; then A6: Cl {y} misses V by A3,TSEP_1:40; x in {x} & {x} c= Cl {x} by PRE_TOPC:48,TARSKI:def 1; then A7: (Cl {x}) /\ V <> {} by A4,XBOOLE_0:def 3; assume Cl {x} = Cl {y}; hence contradiction by A6,A7,XBOOLE_0:def 7; suppose ex W being Subset of X st W is open & not x in W & y in W; then consider W being Subset of X such that A8: W is open and A9: not x in W and A10: y in W; x in W` by A9,SUBSET_1:50; then {x} c= W` by ZFMISC_1:37; then {x} misses W by SUBSET_1:43; then A11: (Cl {x}) misses W by A8,TSEP_1:40; y in {y} & {y} c= Cl {y} by PRE_TOPC:48,TARSKI:def 1; then A12: (Cl {y}) /\ W <> {} by A10,XBOOLE_0:def 3; assume Cl {x} = Cl {y}; hence contradiction by A11,A12,XBOOLE_0:def 7; end; hence Cl {x} <> Cl {y}; end; end; assume A13: for x, y being Point of X st x <> y holds Cl {x} <> Cl {y}; now let x, y be Point of X; assume A14: x <> y; assume A15: for E being Subset of X st E is closed & x in E holds y in E; thus ex F being Subset of X st F is closed & not x in F & y in F proof set F = Cl {y}; take F; thus F is closed by PCOMPS_1:4; now assume x in F; then {x} c= F by ZFMISC_1:37; then A16: Cl {x} c= F by Lm3; x in Cl {x} & Cl {x} is closed by Lm2,PCOMPS_1:4; then y in Cl {x} by A15; then {y} c= Cl {x} by ZFMISC_1:37; then F c= Cl {x} by Lm3; then Cl {x} = F by A16,XBOOLE_0:def 10; hence contradiction by A13,A14; end; hence not x in F; thus y in F by Lm2; end; end; hence X is T_0 by Def4; end; end; definition let X be non empty TopSpace; redefine attr X is T_0 means :Def6: for x, y being Point of X st x <> y holds not x in Cl {y} or not y in Cl {x}; compatibility proof thus X is T_0 implies for x, y being Point of X st x <> y holds not x in Cl {y} or not y in Cl {x} proof assume A1: X is T_0; hereby let x, y be Point of X; assume A2: x <> y; assume x in Cl {y} & y in Cl {x}; then {x} c= Cl {y} & {y} c= Cl {x} by ZFMISC_1:37; then Cl {x} c= Cl {y} & Cl {y} c= Cl {x} by Lm3; then Cl {x} = Cl {y} by XBOOLE_0:def 10; hence contradiction by A1,A2,Def5; end; end; assume A3: for x, y being Point of X st x <> y holds not x in Cl {y} or not y in Cl {x}; for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} proof let x, y be Point of X; assume A4: x <> y; assume A5: Cl {x} = Cl {y}; now per cases by A3,A4; suppose not x in Cl {y}; hence contradiction by A5,Lm2; suppose not y in Cl {x}; hence contradiction by A5,Lm2; end; hence contradiction; end; hence X is T_0 by Def5; end; end; definition let X be non empty TopSpace; redefine attr X is T_0 means for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x}; compatibility proof thus X is T_0 implies for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} proof assume A1: X is T_0; hereby let x, y be Point of X; assume A2: x <> y; assume x in Cl {y}; then {x} c= Cl {y} by ZFMISC_1:37; then A3: Cl {x} c= Cl {y} by Lm3; assume Cl {y} c= Cl {x}; then Cl {x} = Cl {y} by A3,XBOOLE_0:def 10; hence contradiction by A1,A2,Def5; end; end; assume A4: for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x}; for x, y being Point of X st x <> y holds not x in Cl {y} or not y in Cl {x} proof let x, y be Point of X; assume A5: x <> y; assume x in Cl {y}; then A6: not Cl {y} c= Cl {x} by A4,A5; assume y in Cl {x}; then {y} c= Cl {x} by ZFMISC_1:37; hence contradiction by A6,Lm3; end; hence X is T_0 by Def6; end; end; definition cluster almost_discrete T_0 -> discrete (non empty TopSpace); coherence proof let Y be non empty TopSpace; assume A1: Y is almost_discrete T_0; for A being Subset of Y, x being Point of Y st A = {x} holds A is closed proof let A be Subset of Y, x be Point of Y; assume A2: A = {x}; x in Cl {x} by Lm2; then A3: {x} c= Cl {x} by ZFMISC_1:37; now assume not Cl {x} c= {x}; then consider a being set such that A4: a in Cl {x} and A5: not a in {x} by TARSKI:def 3; reconsider a as Point of Y by A4; a <> x by A5,TARSKI:def 1; then not x in Cl {a} by A1,A4,Def6; then x in (Cl {a})` by SUBSET_1:50; then {x} c= (Cl {a})` by ZFMISC_1:37; then A6: {x} misses Cl {a} by SUBSET_1:43; Cl {a} is closed by PCOMPS_1:4; then Cl {a} is open by A1,TDLAT_3:24; then A7: (Cl {x}) misses Cl {a} by A6,TSEP_1:40; a in {a} & {a} c= Cl {a} by PRE_TOPC:48,TARSKI:def 1; hence contradiction by A4,A7,XBOOLE_0:3; end; then Cl {x} = {x} by A3,XBOOLE_0:def 10; hence A is closed by A2,PCOMPS_1:4; end; hence thesis by A1,TDLAT_3:28; end; cluster almost_discrete non discrete -> non T_0 (non empty TopSpace); coherence proof let Y be non empty TopSpace; assume A8: Y is almost_discrete non discrete; assume A9: Y is T_0; for A being Subset of Y, x being Point of Y st A = {x} holds A is closed proof let A be Subset of Y, x be Point of Y; assume A10: A = {x}; x in Cl {x} by Lm2; then A11: {x} c= Cl {x} by ZFMISC_1:37; now assume not Cl {x} c= {x}; then consider a being set such that A12: a in Cl {x} and A13: not a in {x} by TARSKI:def 3; reconsider a as Point of Y by A12; a <> x by A13,TARSKI:def 1; then not x in Cl {a} by A9,A12,Def6; then x in (Cl {a})` by SUBSET_1:50; then {x} c= (Cl {a})` by ZFMISC_1:37; then A14: {x} misses Cl {a} by SUBSET_1:43; Cl {a} is closed by PCOMPS_1:4; then Cl {a} is open by A8,TDLAT_3:24; then A15: (Cl {x}) misses Cl {a} by A14,TSEP_1:40; a in {a} & {a} c= Cl {a} by PRE_TOPC:48,TARSKI:def 1; hence contradiction by A12,A15,XBOOLE_0:3; end; then Cl {x} = {x} by A11,XBOOLE_0:def 10; hence A is closed by A10,PCOMPS_1:4; end; hence contradiction by A8,TDLAT_3:28; end; cluster non discrete T_0 -> non almost_discrete (non empty TopSpace); coherence proof let Y be non empty TopSpace; assume A16: Y is non discrete T_0; assume A17: Y is almost_discrete; for A being Subset of Y, x being Point of Y st A = {x} holds A is closed proof let A be Subset of Y, x be Point of Y; assume A18: A = {x}; x in Cl {x} by Lm2; then A19: {x} c= Cl {x} by ZFMISC_1:37; now assume not Cl {x} c= {x}; then consider a being set such that A20: a in Cl {x} and A21: not a in {x} by TARSKI:def 3; reconsider a as Point of Y by A20; a <> x by A21,TARSKI:def 1; then not x in Cl {a} by A16,A20,Def6; then x in (Cl {a})` by SUBSET_1:50; then {x} c= (Cl {a})` by ZFMISC_1:37; then A22:{x} misses Cl {a} by SUBSET_1:43; Cl {a} is closed by PCOMPS_1:4; then Cl {a} is open by A17,TDLAT_3:24; then A23: (Cl {x}) misses Cl {a} by A22,TSEP_1:40; a in {a} & {a} c= Cl {a} by PRE_TOPC:48,TARSKI:def 1; hence contradiction by A20,A23,XBOOLE_0:3; end; then Cl {x} = {x} by A19,XBOOLE_0:def 10; hence A is closed by A18,PCOMPS_1:4; end; hence contradiction by A16,A17,TDLAT_3:28; end; end; definition mode Kolmogorov_space is T_0 non empty TopSpace; mode non-Kolmogorov_space is non T_0 non empty TopSpace; end; definition cluster non trivial strict Kolmogorov_space; existence proof consider X being non trivial discrete strict (non empty TopSpace); take X; thus thesis; end; cluster non trivial strict non-Kolmogorov_space; existence proof consider X being non trivial anti-discrete strict (non empty TopSpace); take X; thus thesis; end; end; begin :: 3. T_{0} Subsets. definition let Y be TopStruct; let IT be Subset of Y; attr IT is T_0 means :Def8: for x, y being Point of Y st x in IT & y in IT & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; definition let Y be non empty TopStruct; let A be Subset of Y; redefine attr A is T_0 means :Def9: for x, y being Point of Y st x in A & y in A & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); compatibility proof thus A is T_0 implies for x, y being Point of Y st x in A & y in A & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F) proof assume A1: for x, y being Point of Y st x in A & y in A & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); let x, y be Point of Y; assume A2: x in A & y in A & x <> y; hereby per cases by A1,A2; suppose ex V being Subset of Y st V is open & x in V & not y in V; then consider V being Subset of Y such that A3: V is open and A4: x in V and A5: not y in V; now take F = V`; F = [#]Y \ V by PRE_TOPC:17; then V = [#]Y \ F by PRE_TOPC:22; hence F is closed by A3,PRE_TOPC:def 6; thus not x in F by A4,SUBSET_1:54; thus y in F by A5,SUBSET_1:50; end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); suppose ex W being Subset of Y st W is open & not x in W & y in W; then consider W being Subset of Y such that A6: W is open and A7: not x in W and A8: y in W; now take E = W`; E = [#]Y \ W by PRE_TOPC:17; then W = [#]Y \ E by PRE_TOPC:22; hence E is closed by A6,PRE_TOPC:def 6; thus x in E by A7,SUBSET_1:50; thus not y in E by A8,SUBSET_1:54; end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); end; end; assume A9: for x, y being Point of Y st x in A & y in A & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); for x, y being Point of Y st x in A & y in A & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) proof let x, y be Point of Y; assume A10: x in A & y in A & x <> y; hereby per cases by A9,A10; suppose ex E being Subset of Y st E is closed & x in E & not y in E; then consider E being Subset of Y such that A11: E is closed and A12: x in E and A13: not y in E; now take W = E`; W = [#]Y \ E by PRE_TOPC:17; hence W is open by A11,PRE_TOPC:def 6; thus not x in W by A12,SUBSET_1:54; thus y in W by A13,SUBSET_1:50; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose ex F being Subset of Y st F is closed & not x in F & y in F; then consider F being Subset of Y such that A14: F is closed and A15: not x in F and A16: y in F; now take V = F`; V = [#]Y \ F by PRE_TOPC:17; hence V is open by A14,PRE_TOPC:def 6; thus x in V by A15,SUBSET_1:50; thus not y in V by A16,SUBSET_1:54; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; end; hence A is T_0 by Def8; end; end; theorem for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is T_0 implies D1 is T_0 proof let Y0, Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1; assume A1: the TopStruct of Y0 = the TopStruct of Y1; assume A2: D0 = D1; assume A3: D0 is T_0; now let x, y be Point of Y1; assume A4: x in D1 & y in D1; assume A5: x <> y; reconsider x0 = x, y0 = y as Point of Y0 by A1; hereby per cases by A2,A3,A4,A5,Def8; suppose ex V being Subset of Y0 st V is open & x0 in V & not y0 in V; then consider V being Subset of Y0 such that A6: V is open and A7: x0 in V & not y0 in V; reconsider V1 = V as Subset of Y1 by A1; now take V1; V1 in the topology of Y1 by A1,A6,PRE_TOPC:def 5; hence V1 is open by PRE_TOPC:def 5; thus x in V1 & not y in V1 by A7; end; hence (ex V1 being Subset of Y1 st V1 is open & x in V1 & not y in V1) or (ex W1 being Subset of Y1 st W1 is open & not x in W1 & y in W1); suppose ex W being Subset of Y0 st W is open & not x0 in W & y0 in W; then consider W being Subset of Y0 such that A8: W is open and A9: not x0 in W & y0 in W; reconsider W1 = W as Subset of Y1 by A1; now take W1; W1 in the topology of Y1 by A1,A8,PRE_TOPC:def 5; hence W1 is open by PRE_TOPC:def 5; thus not x in W1 & y in W1 by A9; end; hence (ex V1 being Subset of Y1 st V1 is open & x in V1 & not y in V1) or (ex W1 being Subset of Y1 st W1 is open & not x in W1 & y in W1); end; end; hence D1 is T_0 by Def8; end; theorem Th6: for Y being non empty TopStruct, A being Subset of Y st A = the carrier of Y holds A is T_0 iff Y is T_0 proof let Y be non empty TopStruct, A be Subset of Y; assume A1: A = the carrier of Y; hereby assume A is T_0; then for x, y be Point of Y st x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A1,Def8; hence Y is T_0 by Def3; end; hereby assume Y is T_0; then for x, y be Point of Y st x in A & y in A & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by Def3; hence A is T_0 by Def8; end; end; reserve Y for non empty TopStruct; theorem Th7: for A, B being Subset of Y st B c= A holds A is T_0 implies B is T_0 proof let A, B be Subset of Y; assume A1: B c= A; assume A is T_0; then for x, y be Point of Y st x in B & y in B & x <> y holds ((ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W)) by A1,Def8; hence B is T_0 by Def8; end; theorem Th8: for A, B being Subset of Y holds A is T_0 or B is T_0 implies A /\ B is T_0 proof let A, B be Subset of Y; assume A1: A is T_0 or B is T_0; hereby per cases by A1; suppose A2: A is T_0; A /\ B c= A by XBOOLE_1:17; hence A /\ B is T_0 by A2,Th7; suppose A3: B is T_0; A /\ B c= B by XBOOLE_1:17; hence A /\ B is T_0 by A3,Th7; end; end; theorem Th9: for A, B being Subset of Y st A is open or B is open holds A is T_0 & B is T_0 implies A \/ B is T_0 proof let A, B be Subset of Y; assume A1: A is open or B is open; assume A2: A is T_0 & B is T_0; now let x, y be Point of Y; assume A3: x in A \/ B & y in A \/ B; then A4: x in A \/ (B \ A) & y in A \/ (B \ A) by XBOOLE_1:39; A5: x in (A \ B) \/ B & y in (A \ B) \/ B by A3,XBOOLE_1:39; assume A6: x <> y; now per cases by A1; suppose A7: A is open; now per cases by A4,XBOOLE_0:def 2; suppose x in A & y in A; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A2,A6,Def8; suppose A8: x in A & y in B \ A; now take A; thus A is open by A7; thus x in A by A8; thus not y in A by A8,XBOOLE_0:def 4; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose A9: x in B \ A & y in A; now take A; thus A is open by A7; thus not x in A by A9,XBOOLE_0:def 4; thus y in A by A9; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose A10: x in B \ A & y in B \ A; B \ A c= B by XBOOLE_1:36; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A2,A6,A10,Def8 ; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose A11: B is open; now per cases by A5,XBOOLE_0:def 2; suppose A12: x in A \ B & y in A \ B; A \ B c= A by XBOOLE_1:36; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A2,A6,A12,Def8 ; suppose A13: x in A \ B & y in B; now take B; thus B is open by A11; thus not x in B by A13,XBOOLE_0:def 4; thus y in B by A13; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose A14: x in B & y in A \ B; now take B; thus B is open by A11; thus x in B by A14; thus not y in B by A14,XBOOLE_0:def 4; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); suppose x in B & y in B; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) by A2,A6,Def8; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; hence A \/ B is T_0 by Def8; end; theorem Th10: for A, B being Subset of Y st A is closed or B is closed holds A is T_0 & B is T_0 implies A \/ B is T_0 proof let A, B be Subset of Y; assume A1: A is closed or B is closed; assume A2: A is T_0 & B is T_0; now let x, y be Point of Y; assume A3: x in A \/ B & y in A \/ B; then A4: x in A \/ (B \ A) & y in A \/ (B \ A) by XBOOLE_1:39; A5: x in (A \ B) \/ B & y in (A \ B) \/ B by A3,XBOOLE_1:39; assume A6: x <> y; now per cases by A1; suppose A7: A is closed; now per cases by A4,XBOOLE_0:def 2; suppose x in A & y in A; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W) by A2,A6,Def9; suppose A8: x in A & y in B \ A; now take A; thus A is closed by A7; thus x in A by A8; thus not y in A by A8,XBOOLE_0:def 4; end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); suppose A9: x in B \ A & y in A; now take A; thus A is closed by A7; thus not x in A by A9,XBOOLE_0:def 4; thus y in A by A9; end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); suppose A10: x in B \ A & y in B \ A; B \ A c= B by XBOOLE_1:36; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W) by A2,A6,A10,Def9 ; end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); suppose A11: B is closed; now per cases by A5,XBOOLE_0:def 2; suppose A12: x in A \ B & y in A \ B; A \ B c= A by XBOOLE_1:36; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W) by A2,A6,A12,Def9 ; suppose A13: x in A \ B & y in B; now take B; thus B is closed by A11; thus not x in B by A13,XBOOLE_0:def 4; thus y in B by A13; end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); suppose A14: x in B & y in A \ B; now take B; thus B is closed by A11; thus x in B by A14; thus not y in B by A14,XBOOLE_0:def 4; end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); suppose x in B & y in B; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W) by A2,A6,Def9; end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); end; hence (ex V being Subset of Y st V is closed & x in V & not y in V) or (ex W being Subset of Y st W is closed & not x in W & y in W); end; hence A \/ B is T_0 by Def9; end; theorem Th11: for A being Subset of Y holds A is discrete implies A is T_0 proof let A be Subset of Y; assume A1: A is discrete; now let x, y be Point of Y; assume A2: x in A & y in A; then {x} c= A by ZFMISC_1:37; then consider G being Subset of Y such that A3: G is open and A4: A /\ G = {x} by A1,TEX_2:def 5; assume A5: x <> y; now take G; thus G is open by A3; x in {x} by TARSKI:def 1; hence x in G by A4,XBOOLE_0:def 3; now assume y in G; then y in {x} by A2,A4,XBOOLE_0:def 3; hence contradiction by A5,TARSKI:def 1; end; hence not y in G; end; hence (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); end; hence thesis by Def8; end; theorem for A being non empty Subset of Y holds A is anti-discrete & A is not trivial implies A is not T_0 proof let A be non empty Subset of Y; assume A1: A is anti-discrete; assume A2: A is not trivial; consider s being set such that A3: s in A by XBOOLE_0:def 1; reconsider s0 = s as Element of A by A3; A <> {s0} by A2; then consider t being set such that A4: t in A and A5: t <> s0 by ZFMISC_1:41; reconsider s, t as Point of Y by A3,A4; assume A6: A is T_0; now per cases by A4,A5,A6,Def9; suppose ex E being Subset of Y st E is closed & s in E & not t in E; then consider E being Subset of Y such that A7: E is closed and A8: s in E and A9: not t in E; A c= E by A1,A3,A7,A8,TEX_4:def 2; hence contradiction by A4,A9; suppose ex F being Subset of Y st F is closed & not s in F & t in F; then consider F being Subset of Y such that A10: F is closed and A11: not s in F and A12: t in F; A c= F by A1,A4,A10,A12,TEX_4:def 2; hence contradiction by A3,A11; end; hence contradiction; end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :Def10: for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y}; compatibility proof thus A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} proof assume A1: A is T_0; hereby let x, y be Point of X; assume A2: x in A & y in A & x <> y; now per cases by A1,A2,Def8; suppose ex V being Subset of X st V is open & x in V & not y in V; then consider V being Subset of X such that A3: V is open and A4: x in V and A5: not y in V; y in V` by A5,SUBSET_1:50; then {y} c= V` by ZFMISC_1:37; then A6: {y} misses V by SUBSET_1:43; x in {x} & {x} c= Cl {x} by PRE_TOPC:48,TARSKI:def 1; then A7: (Cl {x}) meets V by A4,XBOOLE_0:3; assume Cl {x} = Cl {y}; hence contradiction by A3,A6,A7,TSEP_1:40; suppose ex W being Subset of X st W is open & not x in W & y in W; then consider W being Subset of X such that A8: W is open and A9: not x in W and A10: y in W; x in W` by A9,SUBSET_1:50; then {x} c= W` by ZFMISC_1:37; then A11: {x} misses W by SUBSET_1:43; y in {y} & {y} c= Cl {y} by PRE_TOPC:48,TARSKI:def 1; then A12: (Cl {y}) meets W by A10,XBOOLE_0:3; assume Cl {x} = Cl {y}; hence contradiction by A8,A11,A12,TSEP_1:40; end; hence Cl {x} <> Cl {y}; end; end; assume A13: for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y}; now let x, y be Point of X; assume A14: x in A & y in A & x <> y; assume A15: for E being Subset of X st E is closed & x in E holds y in E; thus ex F being Subset of X st F is closed & not x in F & y in F proof set F = Cl {y}; take F; thus F is closed by PCOMPS_1:4; now assume x in F; then {x} c= F by ZFMISC_1:37; then A16: Cl {x} c= F by Lm3; x in Cl {x} & Cl {x} is closed by Lm2,PCOMPS_1:4; then y in Cl {x} by A15; then {y} c= Cl {x} by ZFMISC_1:37; then F c= Cl {x} by Lm3; then Cl {x} = F by A16,XBOOLE_0:def 10; hence contradiction by A13,A14; end; hence not x in F; thus y in F by Lm2; end; end; hence A is T_0 by Def9; end; end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :Def11: for x, y being Point of X st x in A & y in A & x <> y holds not x in Cl {y} or not y in Cl {x}; compatibility proof thus A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y holds not x in Cl {y} or not y in Cl {x} proof assume A1: A is T_0; hereby let x, y be Point of X; assume A2: x in A & y in A & x <> y; assume x in Cl {y} & y in Cl {x}; then {x} c= Cl {y} & {y} c= Cl {x} by ZFMISC_1:37; then Cl {x} c= Cl {y} & Cl {y} c= Cl {x} by Lm3; then Cl {x} = Cl {y} by XBOOLE_0:def 10; hence contradiction by A1,A2,Def10; end; end; assume A3: for x, y being Point of X st x in A & y in A & x <> y holds not x in Cl {y} or not y in Cl {x}; for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} proof let x, y be Point of X; assume A4: x in A & y in A & x <> y; assume A5: Cl {x} = Cl {y}; now per cases by A3,A4; suppose not x in Cl {y}; hence contradiction by A5,Lm2; suppose not y in Cl {x}; hence contradiction by A5,Lm2; end; hence contradiction; end; hence A is T_0 by Def10; end; end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means for x, y being Point of X st x in A & y in A & x <> y holds x in Cl {y} implies not Cl {y} c= Cl {x}; compatibility proof thus A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y holds x in Cl {y} implies not Cl {y} c= Cl {x} proof assume A1: A is T_0; hereby let x, y be Point of X; assume A2: x in A & y in A & x <> y; assume x in Cl {y}; then {x} c= Cl {y} by ZFMISC_1:37; then A3: Cl {x} c= Cl {y} by Lm3; assume Cl {y} c= Cl {x}; then Cl {x} = Cl {y} by A3,XBOOLE_0:def 10; hence contradiction by A1,A2,Def10; end; end; assume A4: for x, y being Point of X st x in A & y in A & x <> y holds x in Cl {y} implies not Cl {y} c= Cl {x}; for x, y being Point of X st x in A & y in A & x <> y holds not x in Cl {y} or not y in Cl {x} proof let x, y be Point of X; assume A5: x in A & y in A & x <> y; assume x in Cl {y}; then A6: not Cl {y} c= Cl {x} by A4,A5; assume y in Cl {x}; then {y} c= Cl {x} by ZFMISC_1:37; hence contradiction by A6,Lm3; end; hence A is T_0 by Def11; end; end; reserve X for non empty TopSpace; theorem Th13: for A being empty Subset of X holds A is T_0 proof let A be empty Subset of X; A is discrete by TEX_2:35; hence thesis by Th11; end; theorem for x being Point of X holds {x} is T_0 proof let x be Point of X; {x} is discrete by TEX_2:36; hence thesis by Th11; end; begin :: 4. Kolmogorov Subspaces. definition let Y be non empty TopStruct; cluster strict T_0 non empty SubSpace of Y; existence proof consider X0 being trivial strict (non empty SubSpace of Y); take X0; thus thesis; end; end; Lm4: now let Z be TopStruct; let Z0 be SubSpace of Z; [#]Z0 c= [#]Z & [#]Z0 = the carrier of Z0 by PRE_TOPC:12,def 9; hence the carrier of Z0 is Subset of Z by PRE_TOPC:12; end; definition let Y be TopStruct; let Y0 be SubSpace of Y; redefine attr Y0 is T_0 means Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); compatibility proof reconsider A = the carrier of Y0 as Subset of Y by Lm4; thus Y0 is T_0 implies Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W) proof assume A1: Y0 is T_0; hereby assume A2: Y0 is non empty; let x, y be Point of Y; assume x is Point of Y0 & y is Point of Y0; then reconsider x0 = x, y0 = y as Point of Y0; A3: the carrier of Y0 <> {} by A2,STRUCT_0:def 1; assume A4: x <> y; now per cases by A1,A2,A4,Def3; suppose ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0; then consider E0 being Subset of Y0 such that A5: E0 is open and A6: x0 in E0 and A7: not y0 in E0; now consider E being Subset of Y such that A8: E is open and A9: E0 = E /\ A by A5,Def1; take E; thus E is open by A8; E /\ A c= E by XBOOLE_1:17; hence x in E by A6,A9; thus not y in E by A3,A7,A9,XBOOLE_0:def 3; end; hence (ex E being Subset of Y st E is open & x in E & not y in E) or (ex F being Subset of Y st F is open & not x in F & y in F); suppose ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0; then consider F0 being Subset of Y0 such that A10: F0 is open and A11: not x0 in F0 and A12: y0 in F0; now consider F being Subset of Y such that A13: F is open and A14: F0 = F /\ A by A10,Def1; take F; thus F is open by A13; thus not x in F by A3,A11,A14,XBOOLE_0:def 3; F /\ A c= F by XBOOLE_1:17; hence y in F by A12,A14; end; hence (ex E being Subset of Y st E is open & x in E & not y in E) or (ex F being Subset of Y st F is open & not x in F & y in F); end; hence (ex E being Subset of Y st E is open & x in E & not y in E) or (ex F being Subset of Y st F is open & not x in F & y in F); end; end; assume A15: Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or (ex W being Subset of Y st W is open & not x in W & y in W); now assume A16: Y0 is non empty; let x0, y0 be Point of Y0; A17: the carrier of Y0 <> {} by A16,STRUCT_0:def 1; the carrier of Y0 <> {} by A16,STRUCT_0:def 1; then A18: x0 in the carrier of Y0 & y0 in the carrier of Y0; the carrier of Y0 c= the carrier of Y by Def1; then reconsider x = x0, y = y0 as Point of Y by A18; assume A19: x0 <> y0; now per cases by A15,A16,A19; suppose ex E being Subset of Y st E is open & x in E & not y in E; then consider E being Subset of Y such that A20: E is open and A21: x in E and A22: not y in E; now consider E0 being Subset of Y0 such that A23: E0 is open and A24: E0 = E /\ A by A20,Th2; take E0; thus E0 is open by A23; thus x0 in E0 by A17,A21,A24,XBOOLE_0:def 3; now assume A25: y0 in E0; E /\ A c= E by XBOOLE_1:17; hence contradiction by A22,A24,A25; end; hence not y0 in E0; end; hence (ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0) or (ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0); suppose ex F being Subset of Y st F is open & not x in F & y in F; then consider F being Subset of Y such that A26: F is open and A27: not x in F and A28: y in F; now consider F0 being Subset of Y0 such that A29: F0 is open and A30: F0 = F /\ A by A26,Th2; take F0; thus F0 is open by A29; now assume A31: x0 in F0; F /\ A c= F by XBOOLE_1:17; hence contradiction by A27,A30,A31; end; hence not x0 in F0; thus y0 in F0 by A17,A28,A30,XBOOLE_0:def 3; end; hence (ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0) or (ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0); end; hence (ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0) or (ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0); end; hence Y0 is T_0 by Def3; end; end; definition let Y be TopStruct; let Y0 be SubSpace of Y; redefine attr Y0 is T_0 means :Def14: Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); compatibility proof reconsider A = the carrier of Y0 as Subset of Y by Lm4; thus Y0 is T_0 implies Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F) proof assume A1: Y0 is T_0; hereby assume A2: Y0 is not empty; let x, y be Point of Y; assume x is Point of Y0 & y is Point of Y0; then reconsider x0 = x, y0 = y as Point of Y0; A3: the carrier of Y0 <> {} by A2,STRUCT_0:def 1; assume A4: x <> y; now per cases by A1,A2,A4,Def4; suppose ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0; then consider E0 being Subset of Y0 such that A5: E0 is closed and A6: x0 in E0 and A7: not y0 in E0; now consider E being Subset of Y such that A8: E is closed and A9: E0 = E /\ A by A5,Def2; take E; thus E is closed by A8; E /\ A c= E by XBOOLE_1:17; hence x in E by A6,A9; thus not y in E by A3,A7,A9,XBOOLE_0:def 3; end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); suppose ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0; then consider F0 being Subset of Y0 such that A10: F0 is closed and A11: not x0 in F0 and A12: y0 in F0; now consider F being Subset of Y such that A13: F is closed and A14: F0 = F /\ A by A10,Def2; take F; thus F is closed by A13; thus not x in F by A3,A11,A14,XBOOLE_0:def 3; F /\ A c= F by XBOOLE_1:17; hence y in F by A12,A14; end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); end; hence (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); end; end; assume A15: Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F); now assume A16: Y0 is not empty; let x0, y0 be Point of Y0; A17: the carrier of Y0 <> {} by A16,STRUCT_0:def 1; the carrier of Y0 <> {} by A16,STRUCT_0:def 1; then A18: x0 in the carrier of Y0 & y0 in the carrier of Y0; the carrier of Y0 c= the carrier of Y by Def1; then reconsider x = x0, y = y0 as Point of Y by A18; assume A19: x0 <> y0; now per cases by A15,A16,A19; suppose ex E being Subset of Y st E is closed & x in E & not y in E; then consider E being Subset of Y such that A20: E is closed and A21: x in E and A22: not y in E; now consider E0 being Subset of Y0 such that A23: E0 is closed and A24: E0 = E /\ A by A20,Th4; take E0; thus E0 is closed by A23; thus x0 in E0 by A17,A21,A24,XBOOLE_0:def 3; now assume A25: y0 in E0; E /\ A c= E by XBOOLE_1:17; hence contradiction by A22,A24,A25; end; hence not y0 in E0; end; hence (ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0) or (ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0); suppose ex F being Subset of Y st F is closed & not x in F & y in F; then consider F being Subset of Y such that A26: F is closed and A27: not x in F and A28: y in F; now consider F0 being Subset of Y0 such that A29: F0 is closed and A30: F0 = F /\ A by A26,Th4; take F0; thus F0 is closed by A29; now assume A31: x0 in F0; F /\ A c= F by XBOOLE_1:17; hence contradiction by A27,A30,A31; end; hence not x0 in F0; thus y0 in F0 by A17,A28,A30,XBOOLE_0:def 3; end; hence (ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0) or (ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0); end; hence (ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0) or (ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0); end; hence Y0 is T_0 by Def4; end; end; reserve Y for non empty TopStruct; theorem Th15: for Y0 being non empty SubSpace of Y, A being Subset of Y st A = the carrier of Y0 holds A is T_0 iff Y0 is T_0 proof let Y0 be non empty SubSpace of Y, A be Subset of Y; assume A1: A = the carrier of Y0; hereby assume A is T_0; then for x, y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F) by A1,Def9; hence Y0 is T_0 by Def14; end; hereby assume Y0 is T_0; then for x, y be Point of Y st x in A & y in A & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or (ex F being Subset of Y st F is closed & not x in F & y in F) by A1,Def14; hence A is T_0 by Def9; end; end; theorem for Y0 being non empty SubSpace of Y, Y1 being T_0 non empty SubSpace of Y st Y0 is SubSpace of Y1 holds Y0 is T_0 proof let Y0 be non empty SubSpace of Y, Y1 be T_0 non empty SubSpace of Y; the carrier of Y1 is non empty Subset of Y & the carrier of Y0 is non empty Subset of Y by Lm4; then reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty Subset of Y; A1: [#]Y0 = A0 & [#]Y1 = A1 by PRE_TOPC:12; assume Y0 is SubSpace of Y1; then A2: A0 c= A1 by A1,PRE_TOPC:def 9; A1 is T_0 by Th15; then A0 is T_0 by A2,Th7; hence Y0 is T_0 by Th15; end; reserve X for non empty TopSpace; theorem for X1 being T_0 non empty SubSpace of X, X2 being non empty SubSpace of X holds X1 meets X2 implies X1 meet X2 is T_0 proof let X1 be T_0 non empty SubSpace of X, X2 be non empty SubSpace of X; the carrier of X1 is non empty Subset of X by TSEP_1:1; then reconsider A1 = the carrier of X1 as non empty Subset of X ; the carrier of X2 is non empty Subset of X by TSEP_1:1; then reconsider A2 = the carrier of X2 as non empty Subset of X ; assume X1 meets X2; then A1: the carrier of X1 meet X2 = A1 /\ A2 by TSEP_1:def 5; A1 is T_0 by Th15; then A1 /\ A2 is T_0 by Th8; hence thesis by A1,Th15; end; theorem for X1, X2 being T_0 non empty SubSpace of X holds X1 is open or X2 is open implies X1 union X2 is T_0 proof let X1, X2 be T_0 non empty SubSpace of X; the carrier of X1 is non empty Subset of X & the carrier of X2 is non empty Subset of X by TSEP_1:1; then reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of X; assume X1 is open or X2 is open; then A1: A1 is open or A2 is open by TSEP_1:16; A2: the carrier of X1 union X2 = A1 \/ A2 by TSEP_1:def 2; A1 is T_0 & A2 is T_0 by Th15; then A1 \/ A2 is T_0 by A1,Th9; hence thesis by A2,Th15; end; theorem for X1, X2 being T_0 non empty SubSpace of X holds X1 is closed or X2 is closed implies X1 union X2 is T_0 proof let X1, X2 be T_0 non empty SubSpace of X; the carrier of X1 is non empty Subset of X & the carrier of X2 is non empty Subset of X by TSEP_1:1; then reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of X; assume X1 is closed or X2 is closed; then A1: A1 is closed or A2 is closed by TSEP_1:11; A2: the carrier of X1 union X2 = A1 \/ A2 by TSEP_1:def 2; A1 is T_0 & A2 is T_0 by Th15; then A1 \/ A2 is T_0 by A1,Th10; hence thesis by A2,Th15; end; definition let X be non empty TopSpace; mode Kolmogorov_subspace of X is T_0 non empty SubSpace of X; end; theorem for X being non empty TopSpace, A0 being non empty Subset of X st A0 is T_0 ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 proof let X be non empty TopSpace, A0 be non empty Subset of X; assume A1: A0 is T_0; consider X0 being strict non empty SubSpace of X such that A2: A0 = the carrier of X0 by TSEP_1:10; reconsider X0 as strict Kolmogorov_subspace of X by A1,A2,Th15; take X0; thus thesis by A2; end; definition let X be non trivial (non empty TopSpace); cluster proper strict Kolmogorov_subspace of X; existence proof consider X0 being trivial strict (non empty SubSpace of X); take X0; thus thesis; end; end; definition let X be Kolmogorov_space; cluster -> T_0 (non empty SubSpace of X); coherence proof let X0 be non empty SubSpace of X; the carrier of X0 is non empty Subset of X by TSEP_1:1; then reconsider A0 = the carrier of X0 as non empty Subset of X; X is SubSpace of X by TSEP_1:2; then the carrier of X is non empty Subset of X by TSEP_1:1; then reconsider A = the carrier of X as non empty Subset of X; A is T_0 & A0 c= A by Th6; then A0 is T_0 by Th7; hence thesis by Th15; end; end; definition let X be non-Kolmogorov_space; cluster non proper -> non T_0 (non empty SubSpace of X); coherence proof let X0 be non empty SubSpace of X; the carrier of X0 is non empty Subset of X by TSEP_1:1; then reconsider A0 = the carrier of X0 as non empty Subset of X ; X is SubSpace of X by TSEP_1:2; then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1; assume X0 is non proper; then A0 is not proper by TEX_2:13; then A0 = A by TEX_2:5; then A0 is not T_0 by Th6; hence thesis by Th15; end; cluster T_0 -> proper (non empty SubSpace of X); coherence proof let X0 be non empty SubSpace of X; the carrier of X0 is non empty Subset of X by TSEP_1:1; then reconsider A0 = the carrier of X0 as non empty Subset of X ; X is SubSpace of X by TSEP_1:2; then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1; assume A1: X0 is T_0; assume X0 is non proper; then A0 is not proper by TEX_2:13; then A0 = A by TEX_2:5; then A0 is not T_0 by Th6; hence contradiction by A1,Th15; end; end; definition let X be non-Kolmogorov_space; cluster strict non T_0 SubSpace of X; existence proof consider X0 being non proper strict (non empty SubSpace of X); take X0; thus thesis; end; end; definition let X be non-Kolmogorov_space; mode non-Kolmogorov_subspace of X is non T_0 SubSpace of X; end; theorem for X being non empty non-Kolmogorov_space, A0 being Subset of X st A0 is not T_0 ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 proof let X be non empty non-Kolmogorov_space, A0 be Subset of X; assume A1: A0 is not T_0; then A0 is non empty by Th13; then consider X0 being strict non empty SubSpace of X such that A2: A0 = the carrier of X0 by TSEP_1:10; reconsider X0 as non T_0 strict SubSpace of X by A1,A2,Th15; take X0; thus thesis by A2; end;

Back to top