:: On the characterizations of compactness
:: by Grzegorz Bancerek , Noboru Endou and Yuji Sakai
::
:: Received July 29, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, CARD_FIL, YELLOW_1, LATTICES, PRE_TOPC,
CONNSP_2, STRUCT_0, TARSKI, ZFMISC_1, WAYBEL_0, XXREAL_0, TOPS_1,
WAYBEL_7, RCOMP_1, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, SETFAM_1,
LATTICE3, ORDERS_2, WELLORD2, ORDINAL1, MCART_1, YELLOW_6, SEQ_2,
METRIC_1, CANTOR_1, ARYTM_0, ARYTM_3, CLASSES1, INT_2, YELLOW_0, CAT_1,
BHSP_3, YELLOW19;
notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, MCART_1,
SETFAM_1, FINSET_1, FUNCT_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2,
CLASSES1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1,
CONNSP_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1,
WAYBEL_7, YELLOW_6, WAYBEL_9, YELLOW_7, WAYBEL32;
constructors CLASSES1, TOLER_1, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, WAYBEL_1,
WAYBEL_7, WAYBEL32, COMPTS_1, RELSET_1, XTUPLE_0, XFAMILY;
registrations SUBSET_1, RELAT_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_6, WAYBEL_7, WAYBEL_9,
WAYBEL32, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, TOPS_2, WAYBEL_0, WAYBEL_7, WAYBEL_9, XBOOLE_0, FINSET_1;
equalities SUBSET_1, WAYBEL_0, XBOOLE_0, STRUCT_0;
expansions TARSKI, SUBSET_1, TOPS_2, WAYBEL_0, WAYBEL_7, WAYBEL_9, XBOOLE_0,
FINSET_1;
theorems TARSKI, SETFAM_1, FUNCT_2, FINSET_1, FUNCT_1, CLASSES1, RELAT_1,
ZFMISC_1, RELAT_2, SUBSET_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_2,
CANTOR_1, ORDERS_2, 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, FUNCT_1;
begin
reserve x,y,X for set;
theorem Th1:
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:4;
end;
definition
let T be non empty TopSpace;
let x be Point of T;
func NeighborhoodSystem x -> Subset of BoolePoset [#]T equals
the set of all A where A is
a_neighborhood of x;
coherence
proof
set Y = the set of all A where A is a_neighborhood of x;
set X = the carrier of T;
Y c= bool X
proof
let y being object;
assume y in Y;
then ex A being a_neighborhood of x st y = A;
hence thesis;
end;
hence thesis by WAYBEL_7:2;
end;
end;
theorem Th2:
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;
B in NeighborhoodSystem x iff ex A being a_neighborhood of x st B = A;
hence thesis;
end;
registration
let T be non empty TopSpace;
let x be Point of T;
cluster NeighborhoodSystem x -> non empty proper upper filtered;
coherence
proof
set Y = NeighborhoodSystem x;
set X = the carrier of T, L = BoolePoset [#]T;
set A0 = the a_neighborhood of x;
A0 in NeighborhoodSystem x;
hence NeighborhoodSystem x is non empty;
{} c= X;
then
A1: {} in bool X;
{} is not a_neighborhood of x by CONNSP_2:4;
then
A2: not {} in NeighborhoodSystem x by Th2;
the carrier of BoolePoset X = bool X by WAYBEL_7:2;
hence NeighborhoodSystem x is proper by A1,A2;
thus NeighborhoodSystem x is upper
proof
let a,b be Element of L;
reconsider B = b as Subset of T by WAYBEL_7:2;
assume a in Y;
then reconsider A = a as a_neighborhood of x by Th2;
assume a <= b;
then A c= B by YELLOW_1:2;
then
A3: Int A c= Int B by TOPS_1:19;
x in Int A by CONNSP_2:def 1;
then b is a_neighborhood of x by A3,CONNSP_2:def 1;
hence thesis;
end;
let a,b be Element of L;
assume that
A4: a in Y and
A5: b in Y;
reconsider A = a, B = b as a_neighborhood of x by A4,A5,Th2;
A6: A /\ B is a_neighborhood of x by CONNSP_2:2;
then A /\ B in NeighborhoodSystem x;
then reconsider z = A /\ B as Element of L;
take z;
A7: z c= B by XBOOLE_1:17;
z c= A by XBOOLE_1:17;
hence thesis by A6,A7,YELLOW_1:2;
end;
end;
theorem Th3:
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;
let F be upper Subset of BoolePoset [#]T;
hereby
assume
A1: x is_a_convergence_point_of F, T;
thus NeighborhoodSystem x c= F
proof
let y be object;
assume y in NeighborhoodSystem x;
then reconsider y as a_neighborhood of x by Th2;
x in Int y by CONNSP_2:def 1;
then
A2: Int y in F by A1;
Int y c= y by TOPS_1:16;
hence thesis by A2,WAYBEL_7:7;
end;
end;
assume
A3: NeighborhoodSystem x c= F;
let A be Subset of T;
assume that
A4: A is open and
A5: x in A;
A is a_neighborhood of x by A4,A5,CONNSP_2:3;
then A in NeighborhoodSystem x;
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 Th3;
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;
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;
set x = the Element of A \ Int A;
A2: Int A c= A by TOPS_1:16;
assume A is not open;
then not A c= Int A by A2,XBOOLE_0:def 10;
then
A3: A \ Int A <> {} by XBOOLE_1:37;
then x in A \ Int A;
then reconsider x as Point of T;
A4: x in A by A3,XBOOLE_0:def 5;
x is_a_convergence_point_of NeighborhoodSystem x, T by Th3;
then A in NeighborhoodSystem x by A1,A4;
then A is a_neighborhood of x by Th2;
then x in Int A by CONNSP_2:def 1;
hence thesis by A3,XBOOLE_0:def 5;
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
set i = the Element of N;
reconsider A = rng the mapping of N|i as Subset of S;
take A, i;
thus thesis;
end;
end;
theorem
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;
registration
let S be non empty 1-sorted;
let N be reflexive non empty NetStr over S;
cluster -> non empty for Subset of S,N;
coherence
proof
let A be Subset of S,N;
ex i being Element of N st A = rng the mapping of N|i by Def2;
hence thesis;
end;
end;
theorem Th7:
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 object such that
A2: y in the carrier of N|i and
A3: x = (the mapping of N|i).y by A1,FUNCT_1:def 3;
reconsider y as Element of N|i by A2;
consider j being Element of N such that
A4: j = y and
A5: i <= j by WAYBEL_9:def 7;
take j;
thus i <= j by A5;
thus x = (N|i).y by A3
.= N.j by A4,WAYBEL_9:16;
end;
given j being Element of N such that
A6: i <= j and
A7: x = N.j;
reconsider k = j as Element of N|i by A6,WAYBEL_9:def 7;
A8: x = (N|i).k by A7,WAYBEL_9:16
.= (the mapping of N|i).j;
j in the carrier of N|i by A6,WAYBEL_9:def 7;
hence thesis by A1,A8,FUNCT_1:def 3;
end;
theorem Th8:
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 reconsider j9 = j as Element of N|i by WAYBEL_9:def 7;
N.j = (N|i).j9 by WAYBEL_9:16
.= (the mapping of N|i).j9;
hence thesis by A1,FUNCT_2:4;
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;
defpred P[object,object] means
ex i being Element of N st $2 = i & $1 = rng the
mapping of N|i;
let F be finite non empty set such that
A1: for A being Element of F holds A is Subset of S,N;
A2: now
let x be object;
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 object;
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 being object st x in F holds P[x, f.x] from FUNCT_1:sch 6(A2);
reconsider B = rng f as finite Subset of N by A4,FINSET_1:8;
[#]N is directed by 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 Def2;
take C;
let x be object;
A7: the carrier of N|j = {k where k is Element of N: j <= k} by WAYBEL_9:12;
assume x in C;
then consider y being object such that
A8: y in dom the mapping of N|j and
A9: x = (the mapping of N|j).y by FUNCT_1:def 3;
A10: y in the carrier of N|j by A8;
reconsider y as Element of N|j by A8;
consider k being Element of N such that
A11: y = k and
A12: j <= k by A10,A7;
now
let X;
assume
A13: X in F;
then consider i being Element of N such that
A14: f.X = i and
A15: X = rng the mapping of N|i by A5;
i in B by A4,A13,A14,FUNCT_1:def 3;
then i <= j by A6,LATTICE3:def 9;
then i <= k by A12,ORDERS_2:3;
then y in {l where l is Element of N: i <= l} by A11;
then reconsider z = y as Element of N|i by WAYBEL_9:12;
x = (N|j).y by A9
.= N.k by A11,WAYBEL_9:16
.= (N|i).z by A11,WAYBEL_9:16
.= (the mapping of N|i).z;
hence x in X by A15,FUNCT_2:4;
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
{A where A is Subset of
T: N is_eventually_in A};
coherence
proof
set X = the carrier of T;
set F = {A where A is Subset of T: N is_eventually_in A};
A1: F c= bool X
proof
let x be object;
assume x in F;
then ex A being Subset of T st x = A & N is_eventually_in A;
hence thesis;
end;
BoolePoset X = InclPoset bool X by YELLOW_1:4
.= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
hence thesis by A1;
end;
end;
theorem Th10:
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;
B in a_filter N iff ex A being Subset of T st B = A & N is_eventually_in A;
hence thesis;
end;
registration
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 X = the carrier of T, L = BoolePoset [#]T;
set F = a_filter N;
N is_eventually_in [#]T
proof
set i = the Element of N;
take i;
thus thesis;
end;
hence F is non empty by Th10;
let a,b be Element of L;
assume a in F;
then
A1: N is_eventually_in a by Th10;
assume a <= b;
then a c= b by YELLOW_1:2;
then
A2: N is_eventually_in b by A1,WAYBEL_0:8;
BoolePoset X = InclPoset bool X by YELLOW_1:4
.= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
hence thesis by A2;
end;
end;
registration
let T be non empty 1-sorted;
let N be net of T;
cluster a_filter N -> proper filtered;
coherence
proof
set X = the carrier of T, L = BoolePoset [#]T;
set F = a_filter N;
A1: BoolePoset X = InclPoset bool X by YELLOW_1:4
.= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
now
thus {} c= X;
assume {} in F;
then N is_eventually_in {} by Th10;
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds N.j in {};
ex j being Element of N st i <= j & i <= j by YELLOW_6:def 3;
hence contradiction by A2;
end;
then F <> bool X;
hence F is proper by A1;
let a,b be Element of L;
assume that
A3: a in F and
A4: b in F;
N is_eventually_in a by A3,Th10;
then consider i1 being Element of N such that
A5: for j being Element of N st i1 <= j holds N.j in a;
N is_eventually_in b by A4,Th10;
then consider i2 being Element of N such that
A6: for j being Element of N st i2 <= j holds N.j in b;
take z = a"/\"b;
A7: z = a/\b by YELLOW_1:17;
then
A8: z c= b by XBOOLE_1:17;
consider i being Element of N such that
A9: i1 <= i and
A10: i2 <= i by YELLOW_6:def 3;
now
let j be Element of N;
assume
A11: i <= j;
then
A12: N.j in b by A6,A10,ORDERS_2:3;
N.j in a by A5,A9,A11,ORDERS_2:3;
hence N.j in a/\b by A12,XBOOLE_0:def 4;
end;
then N is_eventually_in z by A7;
hence z in F by A1;
z c= a by A7,XBOOLE_1:17;
hence thesis by A8,YELLOW_1:2;
end;
end;
theorem Th11:
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 that
A2: A is open and
A3: x in A;
let B be set;
assume B in F;
then N is_eventually_in B by Th10;
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds N.j in B;
A is a_neighborhood of x by A2,A3,CONNSP_2:3;
then N is_often_in A by A1;
then ex j being Element of N st i <= j & N.j in A;
then ex a being Point of T st a in B & a in A by A4;
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 Def2;
N is_eventually_in B by Th8;
then
A6: B in F;
x in Int O by CONNSP_2:def 1;
then Int O meets B by A5,A6;
then consider x being object such that
A7: x in Int O and
A8: x in B by XBOOLE_0:3;
consider j being Element of N such that
A9: i <= j and
A10: x = N.j by A8,Th7;
take j;
Int O c= O by TOPS_1:16;
hence thesis by A7,A9,A10;
end;
theorem Th12:
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 that
A2: A is open and
A3: x in A;
A is a_neighborhood of x by A2,A3,CONNSP_2:3;
then N is_eventually_in A by A1,YELLOW_6:def 15;
hence thesis;
end;
assume
A4: 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 A4;
then
A5: N is_eventually_in Int O by Th10;
Int O c= O by TOPS_1:16;
hence N is_eventually_in O by A5,WAYBEL_0:8;
end;
hence thesis by YELLOW_6:def 15;
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
deffunc F(object) = $1`1;
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:8;
reconsider f as Subset of L;
consider a being Element of L such that
A1: a in f by SUBSET_1:4;
reconsider a as Element of L;
[a, f] in S by A1;
then reconsider S as non empty set;
defpred P[object,object] 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
RELSET_1:sch 2;
A3: for x being object st x in S holds F(x) in the carrier of L
proof
let x be object;
assume x in S;
then consider a being Element of L, f being Element of F such that
A4: x = [a, f] and
a in f;
thus thesis by A4;
end;
consider h being Function of S, the carrier of L such that
A5: for x being object st x in S holds h.x = F(x) from FUNCT_2:sch 2(A3);
take N=NetStr(#S,R,h#);
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_2:def 5;
end;
hence thesis by A5;
end;
uniqueness
proof
set S = {[a, f] where a is Element of L, f is Element of F: a in f};
let it1,it2 be strict non empty NetStr over L such that
A6: the carrier of it1 = {[a, f] where a is Element of L, f is
Element of F: a in f} and
A7: for i,j being Element of it1 holds i <= j iff j`2 c= i`2 and
A8: for i being Element of it1 holds it1.i = i`1 and
A9: the carrier of it2 = {[a, f] where a is Element of L, f is
Element of F: a in f} and
A10: for i,j being Element of it2 holds i <= j iff j`2 c= i`2 and
A11: for i being Element of it2 holds it2.i = i`1;
A12: for x,y being object holds [x,y] in the InternalRel of it1 iff [x,y] in
the InternalRel of it2
proof
let x,y be object;
hereby
assume
A13: [x,y] in the InternalRel of it1;
then reconsider i=x, j=y as Element of it1 by ZFMISC_1:87;
reconsider i9=x, j9=y as Element of it2 by A6,A9,A13,ZFMISC_1:87;
i <= j by A13,ORDERS_2:def 5;
then (j9)`2 c= (i9)`2 by A7;
then i9 <= j9 by A10;
hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5;
end;
assume
A14: [x,y] in the InternalRel of it2;
then reconsider i=x, j=y as Element of it2 by ZFMISC_1:87;
reconsider i9=x, j9=y as Element of it1 by A6,A9,A14,ZFMISC_1:87;
i <= j by A14,ORDERS_2:def 5;
then (j9)`2 c= (i9)`2 by A10;
then i9 <= j9 by A7;
hence thesis by ORDERS_2:def 5;
end;
the mapping of it1 = the mapping of it2
proof
reconsider f2 =the mapping of it2 as Function of S, the carrier of L by
A9;
reconsider f1 =the mapping of it1 as Function of S, the carrier of L by
A6;
for x being object st x in S holds f1.x = f2.x
proof
let x be object;
assume
A15: x in S;
then reconsider x1 = x as Element of it1 by A6;
reconsider x2 = x as Element of it2 by A9,A15;
reconsider x as Element of S by A15;
f1.x = it1.x1 .=x1`1 by A8
.= it2.x2 by A11;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
hence thesis by A6,A9,A12,RELAT_1:def 2;
end;
end;
registration
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 object
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 object;
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 k=z as Element of a_net F by A3;
reconsider j=y as Element of a_net F by A2;
j <= k by A5,ORDERS_2:def 5;
then
A6: k`2 c= j`2 by Def4;
reconsider i=x as Element of a_net F by A1;
i <= j by A4,ORDERS_2:def 5;
then j`2 c= i`2 by Def4;
then k`2 c= i`2 by A6;
then i <= k by Def4;
hence thesis by ORDERS_2:def 5;
end;
then
A7: the InternalRel of (a_net F) is_transitive_in the carrier of ( a_net
F) by RELAT_2:def 8;
for x being object st x in the carrier of a_net F holds [x,x] in the
InternalRel of a_net F
proof
let x being object;
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_2:def 5;
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 A7,ORDERS_2:def 2,def 3;
end;
end;
registration
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 that
x in [#](a_net F) and
y in [#](a_net F);
x in the carrier of a_net F;
then x in S by Def4;
then consider a being Element of L, f being Element of F such that
A1: x = [a, f] and
a in f;
reconsider f as Element of BoolePoset O;
y in the carrier of a_net F;
then y in S by Def4;
then consider b being Element of L, g being Element of F such that
A2: y = [b, g] and
b in g;
reconsider g as Element of BoolePoset O;
reconsider h = f "/\" g as Element of F by WAYBEL_0:41;
set s = the Element of h;
A3: h c= O by WAYBEL_8:26;
not Bottom (BoolePoset O) in F by WAYBEL_7:4;
then not {} in F by YELLOW_1:18;
then
A4: h <> {};
then s in h;
then s in O by A3;
then reconsider s as Element of L;
[s,h] in S by A4;
then reconsider z = [s,h] as Element of a_net F by Def4;
reconsider i = x, j = y, k = z as Element of a_net F;
A5: [b,g]`2 = g;
take z;
A6: [s,h]`2 = h;
f /\ g c= g by XBOOLE_1:17;
then
A7: h c= g by YELLOW_1:17;
f /\ g c= f by XBOOLE_1:17;
then
A8: h c= f by YELLOW_1:17;
[a,f]`2 = f;
hence thesis by A5,A6,A8,A7,Def4,A1,A2;
end;
then [#](a_net F) is directed;
hence thesis;
end;
end;
theorem Th13:
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;
set X = a_filter a_net F;
A1: the carrier of a_net F = {[a, f] where a is Element of T, f is Element
of F: a in f} by Def4;
A2: BoolePoset [#]T = InclPoset bool [#]T by YELLOW_1:4;
thus F \ {{}} c= X
proof
let x be object;
assume
A3: x in F \ {{}};
then reconsider A = x as Subset of T by A2,YELLOW_1:1;
set a = the Element of A;
not x in {{}} by A3,XBOOLE_0:def 5;
then
A4: A <> {} by TARSKI:def 1;
then a in A;
then reconsider a as Element of T;
x in F by A3,XBOOLE_0:def 5;
then [a, A] in the carrier of a_net F by A1,A4;
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;
A5: (a_net F).j = j`1 by Def4;
assume i <= j;
then
A6: j`2 c= i`2 by Def4;
j in the carrier of a_net F;
then consider a being Element of T, f being Element of F such that
A7: j = [a,f] and
A8: a in f by A1;
A9: j`1 = a by A7;
j`2 = f by A7;
hence thesis by A8,A6,A5,A9;
end;
hence thesis;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A10: x in X;
then a_net F is_eventually_in xx by Th10;
then consider i being Element of a_net F such that
A11: for j being Element of a_net F st i <= j holds (a_net F).j in xx;
i in the carrier of a_net F;
then consider a being Element of T, f being Element of F such that
A12: i = [a,f] and
A13: a in f by A1;
A14: the carrier of BoolePoset [#]T = bool [#]T by A2,YELLOW_1:1;
A15: f c= xx
proof
let x be object;
assume
A16: x in f;
then reconsider b = x as Element of T by A14;
[b,f] in the carrier of a_net F by A1,A16;
then reconsider j = [b,f] as Element of a_net F;
A17: j`2 = f;
j`1 = b;
then
A18: (a_net F).j = b by Def4;
i`2 = f by A12;
then i <= j by A17,Def4;
hence thesis by A11,A18;
end;
x is Subset of T by A10,Th10;
then
A19: x in F by A15,WAYBEL_7:7;
not x in {{}} by A13,A15,TARSKI:def 1;
hence thesis by A19,XBOOLE_0:def 5;
end;
theorem Th14:
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 Th1;
then F \ {{}} = F by ZFMISC_1:57;
hence thesis by Th13;
end;
theorem Th15:
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;
let B be non empty Subset of T;
A1: B in F iff B in F\{{}} by ZFMISC_1:56;
F\{{}} = a_filter a_net F by Th13;
hence thesis by A1,Th10;
end;
theorem Th16:
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 Th14;
hence thesis by 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 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 Th14;
hence thesis by Th12;
end;
theorem Th18:
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;
let i be Element of N;
A3: the carrier of N = {[a, f] where a is Element of T, f is Element of F: a
in f} by Def4;
i in the carrier of N;
then consider a being Element of T, f being Element of F such that
A4: i = [a, f] and
a in f by A3;
reconsider f as a_neighborhood of x by A2,Th2;
A5: i`2 = f by A4;
f meets A by A1,CONNSP_2:27;
then consider b being object such that
A6: b in f and
A7: b in A by XBOOLE_0:3;
reconsider b as Element of T by A6;
[b, f] in the carrier of N by A3,A6;
then reconsider j = [b, f] as Element of N;
take j;
A8: j`1 = b;
j`2 = f;
hence i <= j & N.j in A by A7,A5,A8,Def4;
end;
theorem Th19:
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 Function 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 9;
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 N.(f.p) in A by A1,A4;
hence thesis by A2,FUNCT_2:15;
end;
theorem
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;
theorem Th21:
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 reconsider N = (a_net F)"A as subnet of a_net F by Th18,YELLOW_6:22;
reconsider N9 = N as net of T;
take N9;
thus N9 is_eventually_in A by YELLOW_6:23;
x is_a_convergence_point_of F, T by Th3;
then
A1: x in Lim a_net F by Th17;
Lim a_net F c= Lim N by YELLOW_6:32;
hence x is_a_cluster_point_of N9 by A1,WAYBEL_9:29;
end;
given N being net of T such that
A2: N is_eventually_in A and
A3: x is_a_cluster_point_of N;
consider i being Element of N such that
A4: for j being Element of N st i <= j holds N.j in A by A2;
now
let G be Subset of T;
assume that
A5: G is open and
A6: x in G;
Int G = G by A5,TOPS_1:23;
then G is a_neighborhood of x by A6,CONNSP_2:def 1;
then N is_often_in G by A3;
then consider j being Element of N such that
A7: i <= j and
A8: N.j in G;
N.j in A by A4,A7;
hence A meets G by A8,XBOOLE_0:3;
end;
hence thesis by PRE_TOPC:def 7;
end;
theorem Th22:
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 and
A2: x is_a_cluster_point_of N by Th21;
consider S being subnet of N such that
A3: x in Lim S by A2,WAYBEL_9:32;
reconsider S as convergent net of T by A3,YELLOW_6:def 16;
take S;
thus S is_eventually_in A by A1,Th19;
thus x in Lim S by A3;
end;
given N being convergent net of T such that
A4: N is_eventually_in A and
A5: x in Lim N;
x is_a_cluster_point_of N by A5,WAYBEL_9:29;
hence thesis by A4,Th21;
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:22;
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 Th21;
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:18;
let x be object;
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,Th21;
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:22;
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 Th22;
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:18;
let x be object;
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
,Th22;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th25:
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 and
A2: x is_a_cluster_point_of N by Th21;
set F = a_filter N;
take F;
thus A in F by A1;
thus x is_a_cluster_point_of F, T by A2,Th11;
end;
given F being proper Filter of BoolePoset [#]T such that
A3: A in F and
A4: x is_a_cluster_point_of F, T;
reconsider F9 = F as proper Filter of BoolePoset [#]T;
A5: a_filter a_net F9 = F by Th14;
then
A6: x is_a_cluster_point_of a_net F9 by A4,Th11;
a_net F9 is_eventually_in A by A3,A5,Th10;
hence thesis by A6,Th21;
end;
theorem Th26:
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;
hereby
assume x in Cl A;
then consider N being net of T such that
A1: N is_eventually_in A and
A2: x is_a_cluster_point_of N by Th21;
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 and
A5: G is ultra by WAYBEL_7:26;
reconsider G as ultra Filter of BoolePoset [#]T by A5;
take G;
S is_eventually_in A by A1,Th19;
then A in F;
hence A in G by A4;
x is_a_convergence_point_of F, T by A3,Th12;
hence x is_a_convergence_point_of G, T by A4;
end;
given F being ultra Filter of BoolePoset [#]T such that
A6: A in F and
A7: x is_a_convergence_point_of F, T;
x is_a_cluster_point_of F, T by A7,WAYBEL_7:27;
hence thesis by A6,Th25;
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:22;
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
Th25;
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:18;
let x be object;
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,Th25;
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:22;
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
Th26;
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:18;
let x be object;
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,Th26;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th29:
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;
thus s is_a_cluster_point_of N implies
for A being Subset of T,N holds s in Cl A by Th8,Th21;
assume
A1: 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 Def2;
set x = the Element of A /\ Int V;
A2: s in Int V by CONNSP_2:def 1;
s in Cl A by A1;
then A meets Int V by A2,PRE_TOPC:def 7;
then
A3: A /\ Int V <> {}T;
then
A4: x in Int V by XBOOLE_0:def 4;
A5: Int V c= V by TOPS_1:16;
x in A by A3,XBOOLE_0:def 4;
then consider j being object such that
A6: j in dom the mapping of N|i and
A7: x = (the mapping of N|i).j by FUNCT_1:def 3;
A8: the carrier of N|i = {l where l is Element of N: i <= l} by WAYBEL_9:12;
reconsider j as Element of N|i by A6;
dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1;
then consider l being Element of N such that
A9: j = l and
A10: i <= l by A6,A8;
take l;
thus i <= l by A10;
x = (N|i).j by A7
.= N.l by A9,WAYBEL_9:16;
hence thesis by A4,A5;
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 and
Y is finite and
A3: P = Intersect Y by CANTOR_1:def 3;
A4: P = the carrier of T & the carrier of T = [#]T or P = meet Y by A3,
SETFAM_1:def 9;
for A being Subset of T st A in Y holds A is closed by A1,A2;
hence P is closed by A4,PRE_TOPC:14;
end;
hence thesis;
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 = the set of all Cl A where A is Subset of T, N;
F c= bool the carrier of T
proof
let x be object;
assume x in F;
then ex A being Subset of T, N st x = Cl A;
hence thesis;
end;
then reconsider F as Subset-Family of T;
set x = the Element of meet F;
A2: F is centered
proof
defpred P[object,object] 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;
set A0 = the Subset of T, N;
Cl A0 in F;
hence F <> {};
let G be set such that
A3: G <> {} and
A4: G c= F and
A5: G is finite;
A6: now
let x be object;
assume x in G;
then x in F by A4;
then consider A being Subset of T, N such that
A7: x = Cl A;
consider i being Element of N such that
A8: A = rng the mapping of N|i by Def2;
reconsider y = i as object;
take y;
thus y in the carrier of N;
thus P[x, y] by A7,A8;
end;
consider f being Function such that
A9: dom f = G & rng f c= the carrier of N and
A10: for x being object st x in G holds P[x, f.x] from FUNCT_1:sch 6(A6);
reconsider B = rng f as finite Subset of N by A5,A9,FINSET_1:8;
[#]N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#]N and
A11: j is_>=_than B by WAYBEL_0:1;
now
let X;
assume
A12: X in G;
then consider A being Subset of T,N, i being Element of N such that
A13: X = Cl A and
A14: f.X = i and
A15: A = rng the mapping of N|i by A10;
A16: A c= X by A13,PRE_TOPC:18;
A17: the mapping of N|i = (the mapping of N)|the carrier of (N|i) by
WAYBEL_9:def 7;
i in B by A9,A12,A14,FUNCT_1:def 3;
then i <= j by A11,LATTICE3:def 9;
then j in the carrier of N|i by WAYBEL_9:def 7;
then
A18: j in dom the mapping of N|i by FUNCT_2:def 1;
then (the mapping of N|i).j in A by A15,FUNCT_1:def 3;
then N.j in A by A18,A17,FUNCT_1:47;
hence N.j in X by A16;
end;
hence thesis by A3,SETFAM_1:def 1;
end;
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 thesis;
end;
then
A19: meet F <> {} by A1,A2,COMPTS_1:4;
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 A19,SETFAM_1:def 1;
end;
hence thesis by Th29;
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
set X = the carrier of T;
defpred P[object,object] means ex A being set st A = $1 & $2 in A;
let F be Subset-Family of T such that
A2: F is centered and
A3: F is closed;
set G = FinMeetCl F;
A4: now
let x be object;
reconsider xx = x as set by TARSKI:1;
set y = the Element of xx;
assume x in G;
then consider Y being Subset-Family of T such that
A5: Y c= F and
A6: Y is finite and
A7: x = Intersect Y by CANTOR_1:def 3;
x = the carrier of T or x = meet Y & meet Y <> {} by A2,A5,A6,A7,SETFAM_1
:def 9;
then y in xx;
hence ex y being object st y in the carrier of T & P[x, y] by A7;
end;
consider f being Function such that
A8: dom f = G & rng f c= the carrier of T and
A9: for a being object st a in G holds P[a, f.a] from FUNCT_1:sch 6(A4);
A10: F c= G by CANTOR_1:4;
A11: F <> {} by A2;
then reconsider G as non empty Subset-Family of T by A10;
set R = (InclPoset G) opp;
A12: InclPoset G = RelStr(#G, RelIncl G#) by YELLOW_1:def 1;
then
A13: the carrier of R = G by YELLOW_6:3;
R is directed
proof
let x,y be Element of R such that
x in [#]R and
y in [#]R;
A14: ~x = x by LATTICE3:def 7;
y in G by A13;
then consider Y being Subset-Family of T such that
A15: Y c= F and
A16: Y is finite and
A17: y = Intersect Y by CANTOR_1:def 3;
x in G by A13;
then consider X being Subset-Family of T such that
A18: X c= F and
A19: X is finite and
A20: x = Intersect X by CANTOR_1:def 3;
set z = Intersect (X \/ Y);
X \/ Y c= F by A18,A15,XBOOLE_1:8;
then reconsider z as Element of R by A13,A19,A16,CANTOR_1:def 3;
A21: ~z = z by LATTICE3:def 7;
take z;
thus z in [#]R;
A22: ~y = y by LATTICE3:def 7;
z c= y by A17,SETFAM_1:44,XBOOLE_1:7;
then
A23: ~z <= ~y by A22,A21,YELLOW_1:3;
z c= x by A20,SETFAM_1:44,XBOOLE_1:7;
then ~z <= ~x by A14,A21,YELLOW_1:3;
hence x <= z & y <= z by A23,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 A8,A13,
FUNCT_2:2;
set N = R *' f;
A24: the RelStr of N = the RelStr of R by WAYBEL32:def 3;
A25: the_universe_of X = Tarski-Class the_transitive-closure_of X by
YELLOW_6:def 1;
X c= the_transitive-closure_of X by CLASSES1:52;
then X in Tarski-Class the_transitive-closure_of X by CLASSES1:2,3;
then bool X in Tarski-Class the_transitive-closure_of X by CLASSES1:4;
then G in Tarski-Class the_transitive-closure_of X by CLASSES1:3;
then N in NetUniv T by A13,A24,A25,YELLOW_6:def 11;
then consider x being Point of T such that
A26: x is_a_cluster_point_of N by A1;
A27: the mapping of N = f by WAYBEL32:def 3;
now
let X;
assume
A28: X in F;
then reconsider A = X as Subset of T;
reconsider a = X as Element of N by A10,A12,A24,A28,YELLOW_6:3;
A29: now
let V be Subset of T;
assume that
A30: V is open and
A31: x in V;
Int V = V by A30,TOPS_1:23;
then V is a_neighborhood of x by A31,CONNSP_2:def 1;
then N is_often_in V by A26;
then consider b being Element of N such that
A32: a <= b and
A33: N.b in V;
reconsider a9 = a, b9 = b as Element of (InclPoset G) opp by A24;
a9 <= b9 by A24,A32,YELLOW_0:1;
then
A34: ~a9 >= ~b9 by YELLOW_7:1;
A35: ~b9 = b by LATTICE3:def 7;
~a9 = A by LATTICE3:def 7;
then
A36: b c= A by A34,A35,YELLOW_1:3;
P[b, f.b] by A9,A12,A35;
then N.b in b by A27;
hence A meets V by A33,A36,XBOOLE_0:3;
end;
A is closed by A3,A28;
then Cl A = A by PRE_TOPC:22;
hence x in X by A29,PRE_TOPC:def 7;
end;
hence meet F <> {} by A11,SETFAM_1:def 1;
end;
hence thesis by COMPTS_1:4;
end;
theorem Th31:
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;
hereby
assume
A1: 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 be object;
assume x in G;
then ex A being Subset of T st x = Cl A & A in F;
hence thesis;
end;
then reconsider G as Subset-Family of T;
A2: G is centered
proof
set A0 = the Element of F;
reconsider A0 as Subset of T by WAYBEL_7:2;
Cl A0 in G;
hence G <> {};
let H be set;
assume that
A3: H <> {} and
A4: H c= G and
A5: H is finite;
reconsider H1 = H as finite Subset-Family of X by A4,A5,XBOOLE_1:1;
H1 c= F
proof
let x be object;
assume x in H1;
then x in G by A4;
then consider A being Subset of T such that
A6: x = Cl A and
A7: A in F;
A c= Cl A by PRE_TOPC:18;
hence thesis by A6,A7,WAYBEL_7:7;
end;
then Intersect H1 in F by WAYBEL_7:11;
then Intersect H1 <> {} by Th1;
hence thesis by A3,SETFAM_1:def 9;
end;
set x = the 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
A8: meet G <> {} by A1,A2,COMPTS_1:4;
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
A9: A is open and
A10: x in A;
set B = A`;
A11: now
assume B in F;
then Cl B in G;
then
A12: B in G by A9,PRE_TOPC:22;
not x in B by A10,XBOOLE_0:def 5;
hence contradiction by A8,A12,SETFAM_1:def 1;
end;
F is prime by WAYBEL_7:22;
hence thesis by A11,WAYBEL_7:21;
end;
end;
assume
A13: for F being ultra Filter of BoolePoset [#]T ex x being Point of T
st x is_a_convergence_point_of F, T;
now
set L = BoolePoset X;
let F be Subset-Family of T such that
A14: F is centered closed;
reconsider Y = F as Subset of BoolePoset X by WAYBEL_7:2;
set G = uparrow fininfs Y;
now
assume Bottom L in G;
then consider x being Element of BoolePoset X such that
A15: x <= Bottom L and
A16: x in fininfs Y by WAYBEL_0:def 16;
A17: Bottom L = {} by YELLOW_1:18;
consider Z being finite Subset of Y such that
A18: x = "/\"(Z,L) and
ex_inf_of Z,L by A16;
reconsider Z as Subset of L by XBOOLE_1:1;
A19: x = Bottom L by A15,YELLOW_5:19;
then x <> Top L by WAYBEL_7:3;
then
A20: Z <> {} by A18,YELLOW_0:def 12;
then meet Z <> {} by A14;
hence contradiction by A17,A18,A19,A20,YELLOW_1:20;
end;
then G is proper;
then consider UF being Filter of L such that
A21: G c= UF and
A22: UF is ultra by WAYBEL_7:26;
consider x being Point of T such that
A23: x is_a_convergence_point_of UF, T by A13,A22;
F c= G by WAYBEL_0:62;
then
A24: F c= UF by A21;
A25: now
let A be set;
assume
A26: A in F;
then reconsider B = A as Subset of T;
A27: now
let C be Subset of T;
assume that
A28: C is open and
A29: x in C;
A30: C in UF by A23,A28,A29;
A in UF by A24,A26;
then reconsider c = C, a = A as Element of L by A30;
a"/\"c in UF by A24,A26,A30,WAYBEL_0:41;
then a"/\"c <> {} by A22,Th1;
then A /\ C <> {} by YELLOW_1:17;
hence A meets C;
end;
B is closed by A14,A26;
then Cl B = B by PRE_TOPC:22;
hence x in A by A27,PRE_TOPC:24;
end;
F <> {} by A14;
hence meet F <> {} by A25,SETFAM_1:def 1;
end;
hence thesis by COMPTS_1:4;
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;
hereby
assume
A1: 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
A2: x is_a_cluster_point_of a_net G by A1,Lm1;
take x;
thus x is_a_cluster_point_of F, T by A2,Th16;
end;
assume
A3: 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;
consider x being Point of T such that
A4: x is_a_cluster_point_of F, T by A3;
take x;
thus x is_a_cluster_point_of N by A4,Th11;
end;
hence thesis by Lm2;
end;
theorem Th33:
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;
registration
let L be non empty 1-sorted;
let N be transitive NetStr over L;
cluster -> transitive for full SubNetStr of N;
coherence
proof
let S be full SubNetStr of N;
S is full SubRelStr of N by YELLOW_6:def 7;
hence thesis;
end;
end;
registration
let L be non empty 1-sorted;
let N be non empty directed NetStr over L;
cluster strict non empty directed full for SubNetStr of N;
existence
proof
set S = the NetStr of N;
A1: the RelStr of N = the RelStr of N;
N is full SubRelStr of N by YELLOW_6:6;
then
A2: S is full SubRelStr of N by A1,WAYBEL21:12;
the mapping of S = (the mapping of N)|the carrier of S;
then reconsider S as strict non empty full SubNetStr of N by A2,
YELLOW_6:def 6,def 7;
[#]N is directed by WAYBEL_0:def 6;
then [#]S is directed by A1,WAYBEL_0:3;
then S is directed;
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,Th33;
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 16;
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;
set x = the Element of Lim S;
A6: Lim S <> {} by A5,YELLOW_6:def 16;
then x in Lim S;
then reconsider x as Point of T;
take x;
thus x is_a_cluster_point_of N by A6,WAYBEL_9:29,31;
end;
hence thesis by Th33;
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;
registration
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;
F is prime by WAYBEL_7:22;
then
A1: (A is empty or A is non empty) & (A` is empty or A` is non empty) & A
in F or A` in F by WAYBEL_7:21;
({}S)` = [#]S;
then A` = {}S implies A = [#]S;
hence thesis by A1,Th15,YELLOW_6:20;
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`;
N is_often_in V by A3;
then consider j being Element of N such that
A5: i <= j and
A6: N.j in V;
N.j in V` by A4,A5;
hence contradiction by A6,XBOOLE_0:def 5;
end;
then x in Lim N by YELLOW_6:def 15;
hence thesis by YELLOW_6:def 16;
end;
assume
A7: for N being net of T st N is Cauchy holds N is convergent;
now
let F be ultra Filter of BoolePoset [#]T;
set x = the Element of Lim a_net F;
a_net F is convergent by A7;
then
A8: Lim a_net F <> {} by YELLOW_6:def 16;
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 A8,Th17;
end;
hence thesis by Th31;
end;