### The Mizar article:

### On the Characterizations of Compactness

**by****Grzegorz Bancerek,****Noboru Endou, and****Yuji Sakai**

- Received July 29, 2001
Copyright (c) 2001 Association of Mizar Users

- MML identifier: YELLOW19
- [ MML identifier index ]

environ vocabulary YELLOW_1, ORDERS_1, WELLORD2, COLLSP, FILTER_0, LATTICES, BOOLE, PRE_TOPC, SUBSET_1, CONNSP_2, WAYBEL_0, TOPS_1, WAYBEL_7, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, SETFAM_1, QUANTAL1, LATTICE3, ORDINAL2, MCART_1, YELLOW_6, SEQ_2, SUB_METR, CANTOR_1, COMPTS_1, OPPCAT_1, ARYTM_3, CLASSES1, YELLOW_0, CAT_1, BHSP_3, YELLOW19; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MCART_1, SETFAM_1, FINSET_1, FUNCT_1, RELAT_2, RELSET_1, FUNCT_2, CLASSES1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TEX_2, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, YELLOW_6, WAYBEL_9, YELLOW_7, WAYBEL32; constructors TOLER_1, RELAT_2, WAYBEL_1, CLASSES1, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, WAYBEL_7, WAYBEL32, TEX_2, REALSET1, MEMBERED; clusters SUBSET_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, PUA2MSS1, RELSET_1, RLVECT_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, WAYBEL_9, YELLOW_6, WAYBEL32, MEMBERED, RELAT_1, ZFMISC_1; requirements BOOLE, SUBSET; definitions TARSKI, TOPS_2, COMPTS_1, WAYBEL_0, WAYBEL_7, WAYBEL_9, XBOOLE_0; theorems TARSKI, SETFAM_1, FUNCT_2, FINSET_1, FUNCT_1, CLASSES1, RELAT_1, ZFMISC_1, MCART_1, RELAT_2, SUBSET_1, PRE_TOPC, TOPS_1, TOPS_2, TEX_2, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, WAYBEL_8, WAYBEL_9, YELLOW_5, YELLOW_6, YELLOW_7, WAYBEL12, WAYBEL21, WAYBEL32, XBOOLE_0, XBOOLE_1; schemes RELSET_1, FUNCT_2, COMPTS_1; begin reserve x,y,X for set; canceled; theorem Th2: for X being non empty set for F being proper Filter of BoolePoset X for A being set st A in F holds A is not empty proof let X be non empty set; Bottom BoolePoset X = {} by YELLOW_1:18; hence thesis by WAYBEL_7:8; end; definition let T be non empty TopSpace; let x be Point of T; func NeighborhoodSystem x -> Subset of BoolePoset [#]T equals: Def1: {A where A is a_neighborhood of x: not contradiction}; coherence proof set X = the carrier of T; set Y = {A where A is a_neighborhood of x: not contradiction}; A1: the carrier of BoolePoset X = bool X by WAYBEL_7:4; A2: X = [#]T by PRE_TOPC:12; Y c= bool X proof let y being set; assume y in Y; then ex A being a_neighborhood of x st y = A; hence thesis; end; hence thesis by A1,A2; end; end; theorem Th3: for T being non empty TopSpace, x being Point of T, A being set holds A in NeighborhoodSystem x iff A is a_neighborhood of x proof let T be non empty TopSpace, x be Point of T, B be set; defpred P[] means not contradiction; NeighborhoodSystem x = {A where A is a_neighborhood of x: P[]} by Def1 ; then B in NeighborhoodSystem x iff ex A being a_neighborhood of x st B = A; hence thesis; end; definition let T be non empty TopSpace; let x be Point of T; cluster NeighborhoodSystem x -> non empty proper upper filtered; coherence proof consider A0 being a_neighborhood of x; A0 in NeighborhoodSystem x by Th3; hence NeighborhoodSystem x is non empty; set X = the carrier of T, L = BoolePoset [#]T; set Y = NeighborhoodSystem x; A1: the carrier of BoolePoset X = bool X by WAYBEL_7:4; A2: X = [#]T by PRE_TOPC:12; A3: {} is not a_neighborhood of x by CONNSP_2:6; {} c= X by XBOOLE_1:2; then {} in bool X & not {} in NeighborhoodSystem x by A3,Th3; hence NeighborhoodSystem x is proper by A1,A2,TEX_2:5; thus NeighborhoodSystem x is upper proof let a,b be Element of L; assume a in Y; then reconsider A = a as a_neighborhood of x by Th3; reconsider B = b as Subset of T by A1,A2; assume a <= b; then A c= B by YELLOW_1:2; then Int A c= Int B & x in Int A by CONNSP_2:def 1,TOPS_1:48; then b is a_neighborhood of x by CONNSP_2:def 1; hence thesis by Th3; end; let a,b be Element of L; assume a in Y & b in Y; then reconsider A = a, B = b as a_neighborhood of x by Th3; A4: A /\ B is a_neighborhood of x by CONNSP_2:4; then A /\ B in NeighborhoodSystem x by Th3; then reconsider z = A /\ B as Element of L; take z; z c= A & z c= B by XBOOLE_1:17; hence thesis by A4,Th3,YELLOW_1:2; end; end; theorem Th4: for T being non empty TopSpace, x being Point of T for F being upper Subset of BoolePoset [#]T holds x is_a_convergence_point_of F, T iff NeighborhoodSystem x c= F proof let T be non empty TopSpace, x be Point of T; A1: the carrier of T = [#]T by PRE_TOPC:12; let F be upper Subset of BoolePoset [#]T; hereby assume A2: x is_a_convergence_point_of F, T; thus NeighborhoodSystem x c= F proof let y; assume y in NeighborhoodSystem x; then reconsider y as a_neighborhood of x by Th3; x in Int y by CONNSP_2:def 1; then Int y in F & Int y c= y by A2,TOPS_1:44,WAYBEL_7:def 5; hence thesis by A1,WAYBEL_7:11; end; end; assume A3: NeighborhoodSystem x c= F; let A be Subset of T; assume A is open & x in A; then A is a_neighborhood of x by CONNSP_2:5; then A in NeighborhoodSystem x by Th3; hence thesis by A3; end; theorem for T being non empty TopSpace, x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x, T by Th4; theorem for T being non empty TopSpace for A being Subset of T holds A is open iff for x being Point of T st x in A for F being Filter of BoolePoset [#]T st x is_a_convergence_point_of F, T holds A in F proof let T be non empty TopSpace, A be Subset of T; thus A is open implies for x being Point of T st x in A for F being Filter of BoolePoset [#]T st x is_a_convergence_point_of F, T holds A in F by WAYBEL_7:def 5; assume A1: for x being Point of T st x in A for F being Filter of BoolePoset [#]T st x is_a_convergence_point_of F, T holds A in F; consider x being Element of A \ Int A; assume A is not open; then A <> Int A & Int A c= A by TOPS_1:44; then not A c= Int A by XBOOLE_0:def 10; then A2: A \ Int A <> {} by XBOOLE_1:37; then x in A \ Int A; then reconsider x as Point of T; x is_a_convergence_point_of NeighborhoodSystem x, T & x in A by A2,Th4,XBOOLE_0:def 4; then A in NeighborhoodSystem x by A1; then A is a_neighborhood of x by Th3; then x in Int A by CONNSP_2:def 1; hence thesis by A2,XBOOLE_0:def 4; end; definition let S be non empty 1-sorted; let N be non empty NetStr over S; mode Subset of S,N -> Subset of S means: Def2: ex i being Element of N st it = rng the mapping of N|i; existence proof consider i being Element of N; reconsider A = rng the mapping of N|i as Subset of S; take A, i; thus thesis; end; end; theorem Th7: for S being non empty 1-sorted for N being non empty NetStr over S for i being Element of N holds rng the mapping of N|i is Subset of S, N by Def2; definition let S be non empty 1-sorted; let N be reflexive non empty NetStr over S; cluster -> non empty Subset of S,N; coherence proof let A be Subset of S,N; consider i being Element of N such that A1: A = rng the mapping of N|i by Def2; thus thesis by A1; end; end; theorem Th8: for S being non empty 1-sorted, N being net of S for i being Element of N, x being set holds x in rng the mapping of N|i iff ex j being Element of N st i <= j & x = N.j proof let S be non empty 1-sorted, N be net of S; let i be Element of N, x be set; A1: dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1; hereby assume x in rng the mapping of N|i; then consider y being set such that A2: y in the carrier of N|i & x = (the mapping of N|i).y by A1,FUNCT_1:def 5; reconsider y as Element of N|i by A2; consider j being Element of N such that A3: j = y & i <= j by WAYBEL_9:def 7; take j; thus i <= j by A3; thus x = (N|i).y by A2,WAYBEL_0:def 8 .= N.j by A3,WAYBEL_9:16; end; given j being Element of N such that A4: i <= j & x = N.j; A5: j in the carrier of N|i by A4,WAYBEL_9:def 7; then reconsider k = j as Element of N|i; x = (N|i).k by A4,WAYBEL_9:16 .= (the mapping of N|i).j by WAYBEL_0:def 8 ; hence thesis by A1,A5,FUNCT_1:def 5; end; theorem Th9: for S being non empty 1-sorted, N being net of S for A being Subset of S,N holds N is_eventually_in A proof let S be non empty 1-sorted, N be net of S; let A be Subset of S,N; consider i being Element of N such that A1: A = rng the mapping of N|i by Def2; take i; let j be Element of N; assume i <= j; then j in the carrier of N|i by WAYBEL_9:def 7; then reconsider j' = j as Element of N|i; N.j = (N|i).j' by WAYBEL_9:16 .= (the mapping of N|i).j' by WAYBEL_0:def 8 ; hence thesis by A1,FUNCT_2:6; end; theorem for S being non empty 1-sorted, N being net of S for F being finite non empty set st for A being Element of F holds A is Subset of S,N ex B being Subset of S,N st B c= meet F proof let S be non empty 1-sorted, N be net of S; let F be finite non empty set such that A1: for A being Element of F holds A is Subset of S,N; defpred P[set,set] means ex i being Element of N st $2 = i & $1 = rng the mapping of N|i; A2: now let x; assume x in F; then reconsider A = x as Subset of S, N by A1; consider i being Element of N such that A3: A = rng the mapping of N|i by Def2; reconsider y = i as set; take y; thus y in the carrier of N; thus P[x, y] by A3; end; consider f being Function such that A4: dom f = F & rng f c= the carrier of N and A5: for x st x in F holds P[x, f.x] from NonUniqBoundFuncEx(A2); reconsider B = rng f as finite Subset of N by A4,FINSET_1:26; [#]N is directed & [#]N = the carrier of N by PRE_TOPC:12,WAYBEL_0:def 6; then consider j being Element of N such that j in [#]N and A6: j is_>=_than B by WAYBEL_0:1; reconsider C = rng the mapping of N|j as Subset of S, N by Th7; take C; let x; assume x in C; then consider y such that A7: y in dom the mapping of N|j & x = (the mapping of N|j).y by FUNCT_1:def 5; A8: y in the carrier of N|j by A7; reconsider y as Element of N|j by A7; the carrier of N|j = {k where k is Element of N: j <= k} by WAYBEL_9:12; then consider k being Element of N such that A9: y = k & j <= k by A8; now let X; assume A10: X in F; then consider i being Element of N such that A11: f.X = i & X = rng the mapping of N|i by A5; i in B by A4,A10,A11,FUNCT_1:def 5; then i <= j by A6,LATTICE3:def 9; then i <= k by A9,ORDERS_1:26; then y in {l where l is Element of N: i <= l} by A9; then y in the carrier of N|i by WAYBEL_9:12; then reconsider z = y as Element of N|i; x = (N|j).y by A7,WAYBEL_0:def 8 .= N.k by A9,WAYBEL_9:16 .= (N|i).z by A9,WAYBEL_9:16 .= (the mapping of N|i).z by WAYBEL_0:def 8; hence x in X by A11,FUNCT_2:6; end; hence thesis by SETFAM_1:def 1; end; definition let T be non empty 1-sorted; let N be non empty NetStr over T; func a_filter N -> Subset of BoolePoset [#]T equals: Def3: {A where A is Subset of T: N is_eventually_in A}; coherence proof set F = {A where A is Subset of T: N is_eventually_in A}; set X = the carrier of T; A1: BoolePoset X = InclPoset bool X by YELLOW_1:4 .= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1; A2: [#]T = X by PRE_TOPC:12; F c= bool X proof let x; assume x in F; then ex A being Subset of T st x = A & N is_eventually_in A; hence thesis; end; hence thesis by A1,A2; end; end; theorem Th11: for T being non empty 1-sorted for N being non empty NetStr over T for A being set holds A in a_filter N iff N is_eventually_in A & A is Subset of T proof let T be non empty 1-sorted; let N be non empty NetStr over T; let B be set; a_filter N = {A where A is Subset of T: N is_eventually_in A} by Def3; then B in a_filter N iff ex A being Subset of T st B = A & N is_eventually_in A; hence thesis; end; definition let T be non empty 1-sorted; let N be non empty NetStr over T; cluster a_filter N -> non empty upper; coherence proof set F = a_filter N; set X = the carrier of T, L = BoolePoset [#]T; A1: BoolePoset X = InclPoset bool X by YELLOW_1:4 .= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1; A2: [#]T = X by PRE_TOPC:12; N is_eventually_in [#]T proof consider i being Element of N; take i; thus thesis by A2; end; hence F is non empty by Th11; let a,b be Element of L; assume a in F; then A3: N is_eventually_in a by Th11; assume a <= b; then a c= b by YELLOW_1:2; then b is Subset of T & N is_eventually_in b by A1,A2,A3,WAYBEL_0:8; hence thesis by Th11; end; end; definition let T be non empty 1-sorted; let N be net of T; cluster a_filter N -> proper filtered; coherence proof set F = a_filter N; set X = the carrier of T, L = BoolePoset [#]T; A1: BoolePoset X = InclPoset bool X by YELLOW_1:4 .= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1; A2: [#]T = X by PRE_TOPC:12; now thus {} c= X by XBOOLE_1:2; assume {} in F; then N is_eventually_in {} by Th11; then consider i being Element of N such that A3: for j being Element of N st i <= j holds N.j in {} by WAYBEL_0:def 11; consider j being Element of N such that A4: i <= j & i <= j by YELLOW_6:def 5; thus contradiction by A3,A4; end; then F <> bool X; hence F is proper by A1,A2,TEX_2:5; let a,b be Element of L; assume a in F & b in F; then A5: N is_eventually_in a & N is_eventually_in b by Th11; then consider i1 being Element of N such that A6: for j being Element of N st i1 <= j holds N.j in a by WAYBEL_0:def 11; consider i2 being Element of N such that A7: for j being Element of N st i2 <= j holds N.j in b by A5,WAYBEL_0:def 11; consider i being Element of N such that A8: i1 <= i & i2 <= i by YELLOW_6:def 5; take z = a"/\"b; A9: z = a/\b & z is Subset of T by A1,A2,YELLOW_1:17; now let j be Element of N; assume i <= j; then i1 <= j & i2 <= j by A8,ORDERS_1:26; then N.j in a & N.j in b by A6,A7; hence N.j in a/\b by XBOOLE_0:def 3; end; then N is_eventually_in z by A9,WAYBEL_0:def 11; hence z in F by A9,Th11; z c= a & z c= b by A9,XBOOLE_1:17; hence thesis by YELLOW_1:2; end; end; theorem Th12: for T being non empty TopSpace for N being net of T for x being Point of T holds x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N, T proof let T be non empty TopSpace; let N be net of T; set F = a_filter N; let x be Point of T; thus x is_a_cluster_point_of N implies x is_a_cluster_point_of F, T proof assume A1: for O being a_neighborhood of x holds N is_often_in O; let A be Subset of T; assume A is open & x in A; then A is a_neighborhood of x by CONNSP_2:5; then A2: N is_often_in A by A1; let B be set; assume B in F; then N is_eventually_in B by Th11; then consider i being Element of N such that A3: for j being Element of N st i <= j holds N.j in B by WAYBEL_0:def 11; consider j being Element of N such that A4: i <= j & N.j in A by A2,WAYBEL_0:def 12; now take a = N.j; thus a in B & a in A by A3,A4; end; hence thesis by XBOOLE_0:3; end; assume A5: for A being Subset of T st A is open & x in A for B being set st B in F holds A meets B; let O be a_neighborhood of x; let i be Element of N; reconsider B = rng the mapping of N|i as Subset of T,N by Th7; N is_eventually_in B by Th9; then B in F & x in Int O by Th11,CONNSP_2:def 1; then Int O meets B by A5; then consider x being set such that A6: x in Int O & x in B by XBOOLE_0:3; consider j being Element of N such that A7: i <= j & x = N.j by A6,Th8; take j; Int O c= O by TOPS_1:44; hence thesis by A6,A7; end; theorem Th13: for T being non empty TopSpace for N being net of T for x being Point of T holds x in Lim N iff x is_a_convergence_point_of a_filter N, T proof let T be non empty TopSpace; let N be net of T; set F = a_filter N; let x be Point of T; thus x in Lim N implies x is_a_convergence_point_of F, T proof assume A1: x in Lim N; let A be Subset of T; assume A is open & x in A; then A is a_neighborhood of x by CONNSP_2:5; then N is_eventually_in A by A1,YELLOW_6:def 18; hence thesis by Th11; end; assume A2: for A being Subset of T st A is open & x in A holds A in F; now let O be a_neighborhood of x; x in Int O by CONNSP_2:def 1; then Int O in F by A2; then Int O c= O & N is_eventually_in Int O by Th11,TOPS_1:44; hence N is_eventually_in O by WAYBEL_0:8; end; hence thesis by YELLOW_6:def 18; end; definition let L be non empty 1-sorted; let O be non empty Subset of L; let F be Filter of BoolePoset O; func a_net F -> strict non empty NetStr over L means: Def4: the carrier of it = {[a, f] where a is Element of L, f is Element of F: a in f} & (for i,j being Element of it holds i <= j iff j`2 c= i`2) & for i being Element of it holds it.i = i`1; existence proof set S = {[a, f] where a is Element of L, f is Element of F: a in f}; Top BoolePoset O = O by YELLOW_1:19; then reconsider f = O as Element of F by WAYBEL12:12; reconsider f as Subset of L; consider a being Element of L such that A1:a in f by SUBSET_1:10; reconsider a as Element of L; [a, f] in S by A1; then reconsider S as non empty set; defpred P[set,set] means $2`2 c= $1`2; consider R being Relation of S,S such that A2:for x,y being Element of S holds [x,y] in R iff P[x,y] from Rel_On_Dom_Ex; deffunc F(set) = $1`1; A3:for x being set st x in S holds F(x) in the carrier of L proof let x be set; assume x in S; then consider a being Element of L, f being Element of F such that A4: x = [a, f] & a in f; x`1 = a by A4,MCART_1:def 1; hence thesis; end; consider h being Function of S, the carrier of L such that A5:for x being set st x in S holds h.x = F(x) from Lambda1(A3); take N=NetStr(#S,R,h#); A6:for i,j being Element of N holds i <= j iff j`2 c= i`2 proof let i,j be Element of N; reconsider x = i, y = j as Element of S; [x,y] in the InternalRel of N iff y`2 c= x`2 by A2; hence thesis by ORDERS_1:def 9; end; for i being Element of N holds N.i = i`1 proof let i being Element of N; reconsider x = i as Element of S; h.x = N.i by WAYBEL_0:def 8; hence thesis by A5; end; hence thesis by A6; end; uniqueness proof let it1,it2 be strict non empty NetStr over L such that A7:the carrier of it1 = {[a, f] where a is Element of L, f is Element of F: a in f} and A8:(for i,j being Element of it1 holds i <= j iff j`2 c= i`2) and A9:for i being Element of it1 holds it1.i = i`1 and A10:the carrier of it2 = {[a, f] where a is Element of L, f is Element of F: a in f} and A11:(for i,j being Element of it2 holds i <= j iff j`2 c= i`2) and A12:for i being Element of it2 holds it2.i = i`1; set S = {[a, f] where a is Element of L, f is Element of F: a in f}; A13:the InternalRel of it1 = the InternalRel of it2 proof for x,y being set holds [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 proof let x,y be set; hereby assume A14: [x,y] in the InternalRel of it1; then A15: x in S & y in S by A7,ZFMISC_1:106; then reconsider i=x, j=y as Element of it1 by A7; reconsider i'=x, j'=y as Element of it2 by A10,A15; i <= j by A14,ORDERS_1:def 9; then (j')`2 c= (i')`2 by A8; then i' <= j' by A11; hence [x,y] in the InternalRel of it2 by ORDERS_1:def 9; end; assume A16:[x,y] in the InternalRel of it2; then A17: x in S & y in S by A10,ZFMISC_1:106; then reconsider i=x, j=y as Element of it2 by A10; reconsider i'=x, j'=y as Element of it1 by A7,A17; i <= j by A16,ORDERS_1:def 9; then (j')`2 c= (i')`2 by A11; then i' <= j' by A8; hence [x,y] in the InternalRel of it1 by ORDERS_1:def 9; end; hence thesis by RELAT_1:def 2; end; the mapping of it1 = the mapping of it2 proof reconsider f1 =the mapping of it1 as Function of S, the carrier of L by A7; reconsider f2 =the mapping of it2 as Function of S, the carrier of L by A10 ; for x being set st x in S holds f1.x = f2.x proof let x be set; assume A18:x in S; then reconsider x1 = x as Element of it1 by A7; reconsider x2 = x as Element of it2 by A10,A18; reconsider x as Element of S by A18; f1.x = it1.x1 by WAYBEL_0:def 8 .=x1`1 by A9 .= it2.x2 by A12; hence thesis by WAYBEL_0:def 8; end; hence thesis by FUNCT_2:18; end; hence thesis by A7,A10,A13; end; end; definition let L be non empty 1-sorted; let O be non empty Subset of L; let F be Filter of BoolePoset O; cluster a_net F -> reflexive transitive; coherence proof for x,y,z being set st x in the carrier of a_net F & y in the carrier of a_net F & z in the carrier of a_net F & [x,y] in the InternalRel of a_net F & [y,z] in the InternalRel of a_net F holds [x,z] in the InternalRel of a_net F proof let x,y,z be set; assume that A1:x in the carrier of a_net F and A2: y in the carrier of a_net F and A3: z in the carrier of a_net F and A4: [x,y] in the InternalRel of a_net F and A5: [y,z] in the InternalRel of a_net F; reconsider i=x as Element of a_net F by A1; reconsider j=y as Element of a_net F by A2; reconsider k=z as Element of a_net F by A3; i <= j & j <= k by A4,A5,ORDERS_1:def 9; then j`2 c= i`2 & k`2 c= j`2 by Def4; then k`2 c= i`2 by XBOOLE_1:1; then i <= k by Def4; hence thesis by ORDERS_1:def 9; end; then A6:the InternalRel of (a_net F) is_transitive_in the carrier of (a_net F) by RELAT_2:def 8; for x being set st x in the carrier of a_net F holds [x,x] in the InternalRel of a_net F proof let x being set; assume x in the carrier of a_net F; then reconsider i=x as Element of a_net F; i`2 c= i`2; then i <= i by Def4; hence thesis by ORDERS_1:def 9; end; then the InternalRel of (a_net F) is_reflexive_in the carrier of (a_net F) by RELAT_2:def 1; hence thesis by A6,ORDERS_1:def 4,def 5; end; end; definition let L be non empty 1-sorted; let O be non empty Subset of L; let F be proper Filter of BoolePoset O; cluster a_net F -> directed; coherence proof set S = {[a, f] where a is Element of L, f is Element of F: a in f}; for x,y being Element of a_net F st x in [#](a_net F) & y in [#](a_net F) ex z being Element of a_net F st z in [#](a_net F) & x <= z & y <= z proof let x,y being Element of a_net F; assume x in [#](a_net F) & y in [#](a_net F); x in the carrier of a_net F & y in the carrier of a_net F; then A1: x in S & y in S by Def4; then consider a being Element of L, f being Element of F such that A2: x = [a, f] & a in f; consider b being Element of L, g being Element of F such that A3: y = [b, g] & b in g by A1; reconsider f as Element of BoolePoset O; reconsider g as Element of BoolePoset O; reconsider h = f "/\" g as Element of F by WAYBEL_0:41; consider s being Element of h; not Bottom (BoolePoset O) in F by WAYBEL_7:8; then not {} in F by YELLOW_1:18; then A4: h <> {}; then A5: s in h; h c= O by WAYBEL_8:28; then s in O by A5; then reconsider s as Element of L; [s,h] in S by A4; then A6: [s,h] in the carrier of a_net F by Def4; then reconsider z = [s,h] as Element of a_net F; reconsider i = x, j = y, k = z as Element of a_net F; A7: i`2 = f & j`2 = g & k`2 = h by A2,A3,MCART_1:def 2; h c= f /\ g & f /\ g c= f & f /\ g c= g by XBOOLE_1:17,YELLOW_1:17; then A8: h c= f & h c= g by XBOOLE_1:1; take z; thus thesis by A6,A7,A8,Def4,PRE_TOPC:12; end; then [#](a_net F) is directed by WAYBEL_0:def 1; hence a_net F is directed by WAYBEL_0:def 6; end; end; theorem Th14: for T being non empty 1-sorted for F being Filter of BoolePoset [#]T holds F \ {{}} = a_filter a_net F proof let T be non empty 1-sorted; let F be Filter of BoolePoset [#]T; BoolePoset [#]T = InclPoset bool [#]T by YELLOW_1:4; then A1: the carrier of BoolePoset [#]T = bool [#]T by YELLOW_1:1; A2: [#]T = the carrier of T by PRE_TOPC:12; set X = a_filter a_net F; A3: the carrier of a_net F = {[a, f] where a is Element of T, f is Element of F: a in f} by Def4; thus F \ {{}} c= X proof let x; assume x in F \ {{}}; then A4: x in F & not x in {{}} by XBOOLE_0:def 4; then reconsider A = x as Subset of T by A1,A2; consider a being Element of A; A5: A <> {} by A4,TARSKI:def 1; then a in A; then reconsider a as Element of T; [a, A] in the carrier of a_net F by A3,A4,A5; then reconsider i = [a, A] as Element of a_net F; a_net F is_eventually_in A proof take i; let j be Element of a_net F; j in the carrier of a_net F; then consider a being Element of T, f being Element of F such that A6: j = [a,f] & a in f by A3; assume i <= j; then A7: j`2 c= i`2 & (a_net F).j = j`1 by Def4; j`2 = f & i`2 = A & j`1 = a by A6,MCART_1:7; hence thesis by A6,A7; end; hence thesis by Th11; end; let x; assume x in X; then A8: a_net F is_eventually_in x & x is Subset of T by Th11; then consider i being Element of a_net F such that A9: for j being Element of a_net F st i <= j holds (a_net F).j in x by WAYBEL_0:def 11; i in the carrier of a_net F; then consider a being Element of T, f being Element of F such that A10: i = [a,f] & a in f by A3; A11: f c= x proof let x; assume A12: x in f; then reconsider b = x as Element of T by A1,A2; [b,f] in the carrier of a_net F by A3,A12; then reconsider j = [b,f] as Element of a_net F; j`2 = f & i`2 = f & j`1 = b by A10,MCART_1:7; then i <= j & (a_net F).j = b by Def4; hence thesis by A9; end; then A13: x in F & a in x by A2,A8,A10,WAYBEL_7:11; not x in {{}} by A10,A11,TARSKI:def 1; hence thesis by A13,XBOOLE_0:def 4; end; theorem Th15: for T being non empty 1-sorted for F being proper Filter of BoolePoset [#]T holds F = a_filter a_net F proof let T be non empty 1-sorted; let F be proper Filter of BoolePoset [#]T; not {} in F by Th2; then F \ {{}} = F by ZFMISC_1:65; hence thesis by Th14; end; theorem Th16: for T being non empty 1-sorted for F being Filter of BoolePoset [#]T for A being non empty Subset of T holds A in F iff a_net F is_eventually_in A proof let T be non empty 1-sorted; let F be Filter of BoolePoset [#]T; A1: F\{{}} = a_filter a_net F by Th14; let B be non empty Subset of T; B in F iff B in F\{{}} by ZFMISC_1:64; hence thesis by A1,Th11; end; theorem Th17: for T being non empty TopSpace for F being proper Filter of BoolePoset [#]T for x being Point of T holds x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F, T proof let T be non empty TopSpace; let F be proper Filter of BoolePoset [#]T; F = a_filter a_net F by Th15; hence thesis by Th12; end; theorem Th18: for T being non empty TopSpace for F being proper Filter of BoolePoset [#]T for x being Point of T holds x in Lim a_net F iff x is_a_convergence_point_of F, T proof let T be non empty TopSpace; let F be proper Filter of BoolePoset [#]T; F = a_filter a_net F by Th15; hence thesis by Th13; end; canceled; theorem Th20: for T being non empty TopSpace, x being Point of T, A being Subset of T st x in Cl A for F being proper Filter of BoolePoset [#]T st F = NeighborhoodSystem x holds a_net F is_often_in A proof let T be non empty TopSpace, x be Point of T, A be Subset of T; assume A1: x in Cl A; let F be proper Filter of BoolePoset [#]T such that A2: F = NeighborhoodSystem x; set N = a_net F; A3: the carrier of N = {[a, f] where a is Element of T, f is Element of F: a in f} by Def4; let i be Element of N; i in the carrier of N; then consider a being Element of T, f being Element of F such that A4: i = [a, f] & a in f by A3; reconsider f as a_neighborhood of x by A2,Th3; f meets A by A1,YELLOW_6:6; then consider b being set such that A5: b in f & b in A by XBOOLE_0:3; reconsider b as Element of T by A5; [b, f] in the carrier of N by A3,A5; then reconsider j = [b, f] as Element of N; take j; i`2 = f & j`2 = f & j`1 = b by A4,MCART_1:7; hence i <= j & N.j in A by A5,Def4; end; theorem Th21: for T being non empty 1-sorted, A being set for N being net of T st N is_eventually_in A for S being subnet of N holds S is_eventually_in A proof let T be non empty 1-sorted, A be set; let N be net of T; given i being Element of N such that A1: for j being Element of N st i <= j holds N.j in A; let S be subnet of N; consider f being map of S, N such that A2: the mapping of S = (the mapping of N)*f and A3: for m being Element of N ex n being Element of S st for p being Element of S st n <= p holds m <= f.p by YELLOW_6:def 12; consider n being Element of S such that A4: for p being Element of S st n <= p holds i <= f.p by A3; take n; let p be Element of S; assume n <= p; then i <= f.p by A4; then A5: N.(f.p) in A by A1; S.p = (the mapping of S).p by WAYBEL_0:def 8 .= (the mapping of N).(f.p) by A2,FUNCT_2:21; hence thesis by A5,WAYBEL_0:def 8; end; theorem Th22: for T being non empty TopSpace, F,G,x being set st F c= G & x is_a_convergence_point_of F, T holds x is_a_convergence_point_of G, T proof let T be non empty TopSpace, F,G,x be set such that A1: F c= G and A2: for A being Subset of T st A is open & x in A holds A in F; let A be Subset of T; assume A is open & x in A; then A in F by A2; hence thesis by A1; end; theorem Th23: for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex N being net of T st N is_eventually_in A & x is_a_cluster_point_of N proof let T be non empty TopSpace, A be Subset of T; let x be Point of T; reconsider F = NeighborhoodSystem x as proper Filter of BoolePoset [#]T; hereby assume x in Cl A; then a_net F is_often_in A by Th20; then reconsider N = (a_net F)"A as subnet of a_net F by YELLOW_6:31; reconsider N' = N as net of T; take N'; thus N' is_eventually_in A by YELLOW_6:32; x is_a_convergence_point_of F, T by Th4; then x in Lim a_net F & Lim a_net F c= Lim N by Th18,YELLOW_6:41; hence x is_a_cluster_point_of N' by WAYBEL_9:29; end; given N being net of T such that A1: N is_eventually_in A & x is_a_cluster_point_of N; consider i being Element of N such that A2: for j being Element of N st i <= j holds N.j in A by A1,WAYBEL_0:def 11; now let G be Subset of T; assume A3: G is open & x in G; then Int G = G by TOPS_1:55; then G is a_neighborhood of x by A3,CONNSP_2:def 1; then N is_often_in G by A1,WAYBEL_9:def 9; then consider j being Element of N such that A4: i <= j & N.j in G by WAYBEL_0:def 12; N.j in A by A2,A4; hence A meets G by A4,XBOOLE_0:3; end; hence thesis by PRE_TOPC:def 13; end; theorem Th24: for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex N being convergent net of T st N is_eventually_in A & x in Lim N proof let T be non empty TopSpace, A be Subset of T; let x be Point of T; hereby assume x in Cl A; then consider N being net of T such that A1: N is_eventually_in A & x is_a_cluster_point_of N by Th23; consider S being subnet of N such that A2: x in Lim S by A1,WAYBEL_9:32; reconsider S as convergent net of T by A2,YELLOW_6:def 19; take S; thus S is_eventually_in A by A1,Th21; thus x in Lim S by A2; end; given N being convergent net of T such that A3: N is_eventually_in A & x in Lim N; x is_a_cluster_point_of N by A3,WAYBEL_9:29; hence thesis by A3,Th23; end; theorem for T being non empty TopSpace, A being Subset of T holds A is closed iff for N being net of T st N is_eventually_in A for x being Point of T st x is_a_cluster_point_of N holds x in A proof let T be non empty TopSpace, A be Subset of T; A is closed iff Cl A = A by PRE_TOPC:52; hence A is closed implies for N being net of T st N is_eventually_in A for x being Point of T st x is_a_cluster_point_of N holds x in A by Th23; assume A1: for N being net of T st N is_eventually_in A for x being Point of T st x is_a_cluster_point_of N holds x in A; A = Cl A proof thus A c= Cl A by PRE_TOPC:48; let x; assume A2: x in Cl A; then reconsider y = x as Element of T; ex N being net of T st N is_eventually_in A & y is_a_cluster_point_of N by A2,Th23; hence thesis by A1; end; hence thesis; end; theorem for T being non empty TopSpace, A being Subset of T holds A is closed iff for N being convergent net of T st N is_eventually_in A for x being Point of T st x in Lim N holds x in A proof let T be non empty TopSpace, A be Subset of T; A is closed iff Cl A = A by PRE_TOPC:52; hence A is closed implies for N being convergent net of T st N is_eventually_in A for x being Point of T st x in Lim N holds x in A by Th24; assume A1: for N being convergent net of T st N is_eventually_in A for x being Point of T st x in Lim N holds x in A; A = Cl A proof thus A c= Cl A by PRE_TOPC:48; let x; assume A2: x in Cl A; then reconsider y = x as Element of T; ex N being convergent net of T st N is_eventually_in A & y in Lim N by A2,Th24; hence thesis by A1; end; hence thesis; end; theorem Th27: for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex F being proper Filter of BoolePoset [#]T st A in F & x is_a_cluster_point_of F, T proof let T be non empty TopSpace, A be Subset of T; let x be Point of T; hereby assume x in Cl A; then consider N being net of T such that A1: N is_eventually_in A & x is_a_cluster_point_of N by Th23; set F = a_filter N; take F; thus A in F by A1,Th11; thus x is_a_cluster_point_of F, T by A1,Th12; end; given F being proper Filter of BoolePoset [#]T such that A2: A in F & x is_a_cluster_point_of F, T; reconsider F' = F as proper Filter of BoolePoset [#]T; a_filter a_net F' = F by Th15; then a_net F' is_eventually_in A & x is_a_cluster_point_of a_net F' by A2,Th11,Th12; hence thesis by Th23; end; theorem Th28: for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex F being ultra Filter of BoolePoset [#]T st A in F & x is_a_convergence_point_of F, T proof let T be non empty TopSpace, A be Subset of T; let x be Point of T; set X = the carrier of T; A1: [#]T = X by PRE_TOPC:12; hereby assume x in Cl A; then consider N being net of T such that A2: N is_eventually_in A & x is_a_cluster_point_of N by Th23; consider S being subnet of N such that A3: x in Lim S by A2,WAYBEL_9:32; set F = a_filter S; consider G being Filter of BoolePoset [#]T such that A4: F c= G & G is ultra by WAYBEL_7:30; reconsider G as ultra Filter of BoolePoset [#]T by A4; take G; S is_eventually_in A by A2,Th21; then A in F by Th11; hence A in G by A4; x is_a_convergence_point_of F, T by A3,Th13; hence x is_a_convergence_point_of G, T by A4,Th22; end; given F being ultra Filter of BoolePoset [#]T such that A5: A in F & x is_a_convergence_point_of F, T; x is_a_cluster_point_of F, T by A1,A5,WAYBEL_7:31; hence thesis by A5,Th27; end; theorem for T being non empty TopSpace, A being Subset of T holds A is closed iff for F being proper Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_cluster_point_of F,T holds x in A proof let T be non empty TopSpace, A be Subset of T; A is closed iff Cl A = A by PRE_TOPC:52; hence A is closed implies for F being proper Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_cluster_point_of F,T holds x in A by Th27; assume A1: for F being proper Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_cluster_point_of F,T holds x in A; A = Cl A proof thus A c= Cl A by PRE_TOPC:48; let x; assume A2: x in Cl A; then reconsider y = x as Element of T; ex F being proper Filter of BoolePoset [#]T st A in F & y is_a_cluster_point_of F, T by A2,Th27; hence thesis by A1; end; hence thesis; end; theorem for T being non empty TopSpace, A being Subset of T holds A is closed iff for F being ultra Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_convergence_point_of F,T holds x in A proof let T be non empty TopSpace, A be Subset of T; A is closed iff Cl A = A by PRE_TOPC:52; hence A is closed implies for F being ultra Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_convergence_point_of F,T holds x in A by Th28; assume A1: for F being ultra Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_convergence_point_of F,T holds x in A; A = Cl A proof thus A c= Cl A by PRE_TOPC:48; let x; assume A2: x in Cl A; then reconsider y = x as Element of T; ex F being ultra Filter of BoolePoset [#]T st A in F & y is_a_convergence_point_of F, T by A2,Th28; hence thesis by A1; end; hence thesis; end; theorem Th31: for T being non empty TopSpace, N being net of T for s being Point of T holds s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A proof let T be non empty TopSpace, N be net of T; let s be Point of T; hereby assume A1: s is_a_cluster_point_of N; let A be Subset of T,N; N is_eventually_in A by Th9; hence s in Cl A by A1,Th23; end; assume A2: for A being Subset of T,N holds s in Cl A; let V be a_neighborhood of s; let i be Element of N; reconsider A = rng the mapping of N|i as Subset of T,N by Th7; consider x being Element of A /\ Int V; s in Int V & Int V is open & s in Cl A by A2,CONNSP_2:def 1; then A meets Int V by PRE_TOPC:def 13; then A /\ Int V <> {}T by XBOOLE_0:def 7; then A3: x in A & x in Int V by XBOOLE_0:def 3; then consider j being set such that A4: j in dom the mapping of N|i & x = (the mapping of N|i).j by FUNCT_1:def 5; A5: dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1; reconsider j as Element of N|i by A4; the carrier of N|i = {l where l is Element of N: i <= l} by WAYBEL_9:12; then consider l being Element of N such that A6: j = l & i <= l by A4,A5; take l; thus i <= l by A6; A7: x = (N|i).j by A4,WAYBEL_0:def 8 .= N.l by A6,WAYBEL_9:16; Int V c= V by TOPS_1:44; hence N.l in V by A3,A7; end; theorem for T being non empty TopSpace for F being Subset-Family of T st F is closed holds FinMeetCl F is closed proof let T be non empty TopSpace; let F be Subset-Family of T such that A1: F is closed; now let P be Subset of T; assume P in FinMeetCl F; then consider Y being Subset-Family of T such that A2: Y c= F & Y is finite & P = Intersect Y by CANTOR_1:def 4; A3: for A being Subset of T st A in Y holds A is closed by A1,A2,TOPS_2:def 2; Y = {} or Y <> {}; then P = the carrier of T & the carrier of T = [#]T or P = meet Y by A2,CANTOR_1:def 3,PRE_TOPC:12; hence P is closed by A3,PRE_TOPC:44; end; hence thesis by TOPS_2:def 2; end; Lm1: for T being non empty TopSpace st T is compact for N being net of T ex x being Point of T st x is_a_cluster_point_of N proof let T be non empty TopSpace such that A1: T is compact; let N be net of T; set F = {Cl A where A is Subset of T, N: not contradiction}; F c= bool the carrier of T proof let x; assume x in F; then ex A being Subset of T, N st x = Cl A; hence thesis; end; then F is Subset-Family of T by SETFAM_1:def 7; then reconsider F as Subset-Family of T; consider x being Element of meet F; A2: F is closed proof let S be Subset of T; assume S in F; then ex A being Subset of T,N st S = Cl A; hence S is closed; end; F is centered proof consider A0 being Subset of T, N; Cl A0 in F; hence F <> {}; let G be set such that A3: G <> {} & G c= F & G is finite; defpred P[set,set] means ex A being Subset of T,N, i being Element of N st $1 = Cl A & $2 = i & A = rng the mapping of N|i; A4: now let x; assume x in G; then x in F by A3; then consider A being Subset of T, N such that A5: x = Cl A; consider i being Element of N such that A6: A = rng the mapping of N|i by Def2; reconsider y = i as set; take y; thus y in the carrier of N; thus P[x, y] by A5,A6; end; consider f being Function such that A7: dom f = G & rng f c= the carrier of N and A8: for x st x in G holds P[x, f.x] from NonUniqBoundFuncEx(A4); reconsider B = rng f as finite Subset of N by A3,A7,FINSET_1:26; [#]N is directed & [#]N = the carrier of N by PRE_TOPC:12,WAYBEL_0:def 6; then consider j being Element of N such that j in [#]N and A9: j is_>=_than B by WAYBEL_0:1; now let X; assume A10: X in G; then consider A being Subset of T,N, i being Element of N such that A11: X = Cl A & f.X = i & A = rng the mapping of N|i by A8; i in B by A7,A10,A11,FUNCT_1:def 5; then i <= j by A9,LATTICE3:def 9; then j in the carrier of N|i by WAYBEL_9:def 7; then j in dom the mapping of N|i & the mapping of N|i = (the mapping of N)|the carrier of (N|i) by FUNCT_2:def 1,WAYBEL_9:def 7; then (the mapping of N|i).j in A & (the mapping of N|i).j = (the mapping of N).j by A11,FUNCT_1:70,def 5; then N.j in A & A c= X by A11,PRE_TOPC:48,WAYBEL_0:def 8; hence N.j in X; end; hence meet G <> {} by A3,SETFAM_1:def 1; end; then A12: meet F <> {} by A1,A2,COMPTS_1:13; then x in meet F; then reconsider x as Point of T; take x; now let A be Subset of T,N; Cl A in F; hence x in Cl A by A12,SETFAM_1:def 1; end; hence x is_a_cluster_point_of N by Th31; end; Lm2: for T being non empty TopSpace st for N being net of T st N in NetUniv T ex x being Point of T st x is_a_cluster_point_of N holds T is compact proof let T be non empty TopSpace; assume A1: for N being net of T st N in NetUniv T ex x being Point of T st x is_a_cluster_point_of N; now let F be Subset-Family of T such that A2: F is centered & F is closed; set G = FinMeetCl F; defpred P[set,set] means $2 in $1; A3: now let x; assume x in G; then consider Y being Subset-Family of T such that A4: Y c= F & Y is finite & x = Intersect Y by CANTOR_1:def 4; consider y being Element of x; Y = {} or Y <> {}; then x = the carrier of T or x = meet Y & meet Y <> {} by A2,A4,CANTOR_1:def 3,COMPTS_1:def 2; then y in x; hence ex y st y in the carrier of T & P[x, y] by A4; end; consider f being Function such that A5: dom f = G & rng f c= the carrier of T and A6: for a being set st a in G holds P[a, f.a] from NonUniqBoundFuncEx(A3); A7: F <> {} & F c= G by A2,CANTOR_1:4,COMPTS_1:def 2; then reconsider G as non empty Subset-Family of T by XBOOLE_1:3; set R = (InclPoset G) opp; A8: InclPoset G = RelStr(#G, RelIncl G#) by YELLOW_1:def 1; then A9: the carrier of R = G by YELLOW_6:12; R is directed proof let x,y be Element of R such that x in [#]R & y in [#]R; x in G by A9; then consider X being Subset-Family of T such that A10: X c= F & X is finite & x = Intersect X by CANTOR_1:def 4; y in G by A9; then consider Y being Subset-Family of T such that A11: Y c= F & Y is finite & y = Intersect Y by CANTOR_1:def 4; set z = Intersect (X \/ Y); X \/ Y c= F & X \/ Y is finite by A10,A11,FINSET_1:14,XBOOLE_1:8; then z in G by CANTOR_1:def 4; then reconsider z as Element of R by A9; take z; z in the carrier of R; hence z in [#]R by PRE_TOPC:12; X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7; then z c= x & z c= y & ~x = x & ~y = y & ~z = z by A10,A11,CANTOR_1:11,LATTICE3:def 7; then ~z <= ~x & ~z <= ~y by YELLOW_1:3; hence x <= z & y <= z by YELLOW_7:1; end; then reconsider R as directed non empty transitive RelStr; reconsider f as Function of the carrier of R, the carrier of T by A5,A9,FUNCT_2:4; set N = R *' f; A12: the RelStr of N = the RelStr of R & the mapping of N = f by WAYBEL32:def 3; set X = the carrier of T; A13: the_universe_of X = Tarski-Class the_transitive-closure_of X by YELLOW_6:def 3; X c= the_transitive-closure_of X & the_transitive-closure_of X in Tarski-Class the_transitive-closure_of X by CLASSES1:5,59; then X in Tarski-Class the_transitive-closure_of X by CLASSES1:6; then bool X in Tarski-Class the_transitive-closure_of X by CLASSES1:7; then G in Tarski-Class the_transitive-closure_of X by CLASSES1:6; then N in NetUniv T by A9,A12,A13,YELLOW_6:def 14; then consider x being Point of T such that A14: x is_a_cluster_point_of N by A1; now let X; assume A15: X in F; then reconsider a = X as Element of N by A7,A9,A12; reconsider A = X as Subset of T by A15; A is closed by A2,A15,TOPS_2:def 2; then A16: Cl A = A by PRE_TOPC:52; now let V be Subset of T; assume A17: V is open & x in V; then Int V = V by TOPS_1:55; then V is a_neighborhood of x by A17,CONNSP_2:def 1; then N is_often_in V by A14,WAYBEL_9:def 9; then consider b being Element of N such that A18: a <= b & N.b in V by WAYBEL_0:def 12; reconsider a' = a, b' = b as Element of (InclPoset G) opp by A12; A19: N.b = f.b by A12,WAYBEL_0:def 8; a' <= b' by A12,A18,YELLOW_0:1; then ~a' >= ~b' & ~a' = A & ~b' = b by LATTICE3:def 7,YELLOW_7:1; then b c= A & N.b in b by A6,A8,A19,YELLOW_1:3; hence A meets V by A18,XBOOLE_0:3; end; hence x in X by A16,PRE_TOPC:def 13; end; hence meet F <> {} by A7,SETFAM_1:def 1; end; hence thesis by COMPTS_1:13; end; theorem Th33: for T being non empty TopSpace holds T is compact iff for F being ultra Filter of BoolePoset [#]T ex x being Point of T st x is_a_convergence_point_of F, T proof let T be non empty TopSpace; set X = the carrier of T; A1: the carrier of BoolePoset X = bool X by WAYBEL_7:4; A2: [#]T = X by PRE_TOPC:12; hereby assume A3: T is compact; let F be ultra Filter of BoolePoset [#]T; set G = {Cl A where A is Subset of T: A in F}; G c= bool the carrier of T proof let x; assume x in G; then ex A being Subset of T st x = Cl A & A in F; hence thesis; end; then G is Subset-Family of T by SETFAM_1:def 7; then reconsider G as Subset-Family of T; A4: G is centered proof consider A0 being Element of F; reconsider A0 as Subset of T by A1,A2; Cl A0 in G; hence G <> {}; let H be set; assume A5: H <> {} & H c= G & H is finite; then H c= bool X by XBOOLE_1:1; then reconsider H1 = H as finite Subset-Family of X by A5,SETFAM_1:def 7; H1 c= F proof let x; assume x in H1; then x in G by A5; then consider A being Subset of T such that A6: x = Cl A & A in F; A c= Cl A by PRE_TOPC:48; hence thesis by A2,A6,WAYBEL_7:11; end; then Intersect H1 in F by A2,WAYBEL_7:15; then Intersect H1 <> {} by Th2; hence meet H <> {} by A5,CANTOR_1:def 3; end; consider x being Element of meet G; G is closed proof let A be Subset of T; assume A in G; then ex B being Subset of T st A = Cl B & B in F; hence thesis; end; then A7: meet G <> {} by A3,A4,COMPTS_1:13; then x in meet G; then reconsider x as Point of T; take x; thus x is_a_convergence_point_of F, T proof let A be Subset of T such that A8: A is open & x in A; A9: F is prime by WAYBEL_7:26; set B = A`; [#]T = X by PRE_TOPC:12; then A10: B = X\A by PRE_TOPC:17; now assume B in F; then Cl B in G & B is closed by A8,TOPS_1:30; then B in G & not x in B by A8,A10,PRE_TOPC:52,XBOOLE_0:def 4; hence contradiction by A7,SETFAM_1:def 1; end; hence A in F by A2,A9,A10,WAYBEL_7:25; end; end; assume A11: for F being ultra Filter of BoolePoset [#]T ex x being Point of T st x is_a_convergence_point_of F, T; now let F be Subset-Family of T such that A12: F is centered closed; reconsider Y = F as Subset of BoolePoset X by A1; set L = BoolePoset X; set G = uparrow fininfs Y; now assume Bottom L in G; then consider x being Element of BoolePoset X such that A13: x <= Bottom L & x in fininfs Y by WAYBEL_0:def 16; A14: Bottom L = {} by YELLOW_1:18; fininfs Y = {"/\"(Z,L) where Z is finite Subset of Y: ex_inf_of Z,L} by WAYBEL_0:def 28; then consider Z being finite Subset of Y such that A15: x = "/\"(Z,L) & ex_inf_of Z,L by A13; Z c= the carrier of L by XBOOLE_1:1; then reconsider Z as Subset of L; A16: x = Bottom L by A13,YELLOW_5:22; then x <> Top L by WAYBEL_7:5; then A17: Z <> {} by A15,YELLOW_0:def 12; then meet Z <> {} by A12,COMPTS_1:def 2; hence contradiction by A14,A15,A16,A17,YELLOW_1:20; end; then G is proper by WAYBEL_7:8; then consider UF being Filter of L such that A18: G c= UF & UF is ultra by WAYBEL_7:30; consider x being Point of T such that A19: x is_a_convergence_point_of UF, T by A2,A11,A18; A20: F <> {} by A12,COMPTS_1:def 2; F c= G by WAYBEL_0:62; then A21: F c= UF by A18,XBOOLE_1:1; now let A be set; assume A22: A in F; then reconsider B = A as Subset of T; A23: now let C be Subset of T; assume C is open & x in C; then A24: C in UF & A in UF by A19,A21,A22,WAYBEL_7:def 5; then reconsider c = C, a = A as Element of L; a"/\"c in UF & UF is ultra Filter of L by A18,A24,WAYBEL_0:41; then a"/\"c <> {} by Th2; then A /\ C <> {} by YELLOW_1:17; hence A meets C by XBOOLE_0:def 7; end; B is closed by A12,A22,TOPS_2:def 2; then Cl B = B by PRE_TOPC:52; hence x in A by A23,PRE_TOPC:54; end; hence meet F <> {} by A20,SETFAM_1:def 1; end; hence thesis by COMPTS_1:13; end; theorem for T being non empty TopSpace holds T is compact iff for F being proper Filter of BoolePoset [#]T ex x being Point of T st x is_a_cluster_point_of F, T proof let T be non empty TopSpace; A1: the carrier of T = [#]T by PRE_TOPC:12; hereby assume A2: T is compact; let F be proper Filter of BoolePoset [#]T; reconsider G = F as proper Filter of BoolePoset [#]T; consider x being Point of T such that A3: x is_a_cluster_point_of a_net G by A2,Lm1; take x; thus x is_a_cluster_point_of F, T by A3,Th17; end; assume A4: for F being proper Filter of BoolePoset [#]T ex x being Point of T st x is_a_cluster_point_of F, T; now let N be net of T such that N in NetUniv T; reconsider F = a_filter N as proper Filter of BoolePoset the carrier of T by A1; consider x being Point of T such that A5: x is_a_cluster_point_of F, T by A4; take x; thus x is_a_cluster_point_of N by A5,Th12; end; hence thesis by Lm2; end; theorem Th35: for T being non empty TopSpace holds T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N proof let T be non empty TopSpace; thus T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N by Lm1; assume for N being net of T ex x being Point of T st x is_a_cluster_point_of N; then for N being net of T st N in NetUniv T ex x being Point of T st x is_a_cluster_point_of N; hence thesis by Lm2; end; theorem for T being non empty TopSpace holds T is compact iff for N being net of T st N in NetUniv T ex x being Point of T st x is_a_cluster_point_of N by Lm1,Lm2; definition let L be non empty 1-sorted; let N be transitive NetStr over L; cluster -> transitive (full SubNetStr of N); coherence proof let S be full SubNetStr of N; S is full SubRelStr of N by YELLOW_6:def 9; hence thesis; end; end; definition let L be non empty 1-sorted; let N be non empty directed NetStr over L; cluster strict non empty directed full SubNetStr of N; existence proof set S = the NetStr of N; A1: N is SubNetStr of N & the RelStr of N = the RelStr of N & the RelStr of S = the RelStr of S & N is full SubRelStr of N by YELLOW_6:15,17; then the mapping of S = (the mapping of N)|the carrier of S & S is full SubRelStr of N by WAYBEL21:12,YELLOW_6:def 8; then reconsider S as strict non empty full SubNetStr of N by YELLOW_6:def 8,def 9; S is directed proof [#]N = the carrier of N & [#]S = the carrier of S & [#]N is directed by PRE_TOPC:12,WAYBEL_0:def 6; hence [#]S is directed by A1,WAYBEL_0:3; end; hence thesis; end; end; theorem for T being non empty TopSpace holds T is compact iff for N being net of T ex S being subnet of N st S is convergent proof let T be non empty TopSpace; hereby assume A1: T is compact; let N be net of T; consider x being Point of T such that A2: x is_a_cluster_point_of N by A1,Th35; consider S being subnet of N such that A3: x in Lim S by A2,WAYBEL_9:32; take S; thus S is convergent by A3,YELLOW_6:def 19; end; assume A4: for N being net of T ex S being subnet of N st S is convergent; now let N be net of T; consider S being subnet of N such that A5: S is convergent by A4; consider x being Element of Lim S; A6: Lim S <> {} by A5,YELLOW_6:def 19; then x in Lim S; then reconsider x as Point of T; take x; x is_a_cluster_point_of S by A6,WAYBEL_9:29; hence x is_a_cluster_point_of N by WAYBEL_9:31; end; hence thesis by Th35; end; definition let S be non empty 1-sorted; let N be non empty NetStr over S; attr N is Cauchy means for A being Subset of S holds N is_eventually_in A or N is_eventually_in A` ; end; definition let S be non empty 1-sorted; let F be ultra Filter of BoolePoset [#]S; cluster a_net F -> Cauchy; coherence proof let A be Subset of S; A1: [#]S = the carrier of S by PRE_TOPC:12; A2: ({}S)` = [#]S by PRE_TOPC:27; then A3: A` = {}S implies A = [#]S; F is prime by WAYBEL_7:26; then A in F or (the carrier of S)\A in F by A1,WAYBEL_7:25; then (A is empty or A is non empty) & (A` is empty or A` is non empty) & A in F or A` in F by A1,PRE_TOPC:17; hence thesis by A1,A2,A3,Th16,YELLOW_6:29; end; end; theorem for T being non empty TopSpace holds T is compact iff for N being net of T st N is Cauchy holds N is convergent proof let T be non empty TopSpace; thus T is compact implies for N being net of T st N is Cauchy holds N is convergent proof assume A1: T is compact; let N be net of T such that A2: for A being Subset of T holds N is_eventually_in A or N is_eventually_in A`; consider x being Point of T such that A3: x is_a_cluster_point_of N by A1,Lm1; now let V be a_neighborhood of x; assume not N is_eventually_in V; then N is_eventually_in V` by A2; then consider i being Element of N such that A4: for j being Element of N st i <= j holds N.j in V` by WAYBEL_0:def 11; N is_often_in V by A3,WAYBEL_9:def 9; then consider j being Element of N such that A5: i <= j & N.j in V by WAYBEL_0:def 12; N.j in V` by A4,A5; hence contradiction by A5,YELLOW_6:10; end; then x in Lim N by YELLOW_6:def 18; hence N is convergent by YELLOW_6:def 19; end; assume A6: for N being net of T st N is Cauchy holds N is convergent; now let F be ultra Filter of BoolePoset [#]T; consider x being Element of Lim a_net F; a_net F is convergent by A6; then A7: Lim a_net F <> {} by YELLOW_6:def 19; then x in Lim a_net F; then reconsider x as Point of T; take x; thus x is_a_convergence_point_of F, T by A7,Th18; end; hence T is compact by Th33; end;

Back to top