Copyright (c) 2001 Association of Mizar Users
environ
vocabulary ORDERS_1, FILTER_0, YELLOW_1, ORDINAL2, LATTICES, BHSP_3, WAYBEL_0,
YELLOW_0, WAYBEL_9, PRE_TOPC, WAYBEL28, YELLOW_6, SETFAM_1, TARSKI,
BOOLE, REALSET1, FUNCT_1, SUBSET_1, QUANTAL1, RELAT_2, YELLOW_9,
LATTICE3, RELAT_1, YELLOW_2, COLLSP, YELLOW19, MCART_1, CLASSES1,
ZF_LANG, SUB_METR, FINSET_1, PROB_1, CANTOR_1, PRELAMB, DIRAF, WAYBEL19,
WAYBEL11, WAYBEL_7, COMPTS_1, URYSOHN1, WAYBEL33, RLVECT_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, ORDERS_1, FINSET_1,
RELAT_1, RELSET_1, REALSET1, FUNCT_1, FUNCT_2, SETFAM_1, STRUCT_0,
PRE_TOPC, TEX_2, LATTICE3, YELLOW_0, CARD_FIL, CLASSES1, CLASSES2,
CANTOR_1, WAYBEL_0, YELLOW_1, YELLOW_6, YELLOW_2, WAYBEL_3, WAYBEL_7,
WAYBEL_9, WAYBEL11, COMPTS_1, URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL28,
YELLOW19;
constructors WAYBEL_3, TOLER_1, WAYBEL_1, CANTOR_1, WAYBEL_7, TEX_2, REALSET1,
URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL17, CARD_FIL, CLASSES1, WAYBEL28,
YELLOW19, GROUP_1, TDLAT_3, CLASSES2, MEMBERED, TOPS_2;
clusters SUBSET_1, STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, TOPS_1, FUNCT_1,
LATTICE3, WAYBEL_7, FINSET_1, YELLOW11, YELLOW13, PUA2MSS1, YELLOW_6,
YELLOW_9, WAYBEL19, CLASSES2, WAYBEL28, WAYBEL29, YELLOW19, MEMBERED,
RELAT_1, ZFMISC_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, LATTICE3, YELLOW_6, WAYBEL_0, WAYBEL_7,
YELLOW_9, XBOOLE_0;
theorems TARSKI, WAYBEL_7, WAYBEL_9, YELLOW_0, YELLOW_2, WAYBEL_0, PRE_TOPC,
STRUCT_0, LATTICE3, YELLOW_1, WAYBEL_8, ZFMISC_1, FUNCT_1, FUNCT_2,
YELLOW_9, WAYBEL28, YELLOW_6, SUBSET_1, MCART_1, WAYBEL23, WAYBEL21,
CANTOR_1, TOPS_1, WAYBEL11, FRECHET2, REALSET1, CLASSES1, CLASSES2,
WAYBEL12, YELLOW_4, FINSET_1, SETFAM_1, WAYBEL19, WAYBEL32, YELLOW19,
XBOOLE_0, XBOOLE_1;
schemes COMPTS_1, YELLOW_2;
begin
reserve x for set;
definition
let L be non empty Poset;
let X be non empty Subset of L;
let F be Filter of BoolePoset X;
func lim_inf F -> Element of L equals :Def1:
"\/"({inf B where B is Subset of L: B in F},L);
correctness;
end;
theorem
for L1, L2 being complete LATTICE st the RelStr of L1 = the RelStr of L2
for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of BoolePoset X1, F2 being Filter of BoolePoset X2
st F1 = F2
holds lim_inf F1 = lim_inf F2
proof
let L1,L2 be complete LATTICE such that
A1:the RelStr of L1 = the RelStr of L2;
let X1 be non empty Subset of L1;
let X2 be non empty Subset of L2;
let F1 be Filter of BoolePoset X1, F2 be Filter of BoolePoset X2 such that
A2:F1 = F2;
set Y1 = {inf B1 where B1 is Subset of L1: B1 in F1};
set Y2 = {inf B2 where B2 is Subset of L2: B2 in F2};
A3:lim_inf F1 = "\/"(Y1,L1) by Def1;
A4:lim_inf F2 = "\/"(Y2,L2) by Def1;
A5:Y1 c= Y2
proof
let x; assume x in Y1;
then consider B1 being Subset of L1 such that
A6: x = inf B1 & B1 in F1;
F2 c= the carrier of BoolePoset X2;
then F2 c= bool X2 & X2 c= the carrier of L2 by WAYBEL_7:4;
then B1 c= the carrier of L2 by A2,A6,XBOOLE_1:1;
then reconsider B2=B1 as Subset of L2;
ex_inf_of B1,L1 by YELLOW_0:17;
then inf B1 = inf B2 by A1,YELLOW_0:27;
hence thesis by A2,A6;
end;
Y2 c= Y1
proof
let x; assume x in Y2;
then consider B2 being Subset of L2 such that
A7: x = inf B2 & B2 in F2;
F1 c= the carrier of BoolePoset X1;
then F1 c= bool X1 & X1 c= the carrier of L1 by WAYBEL_7:4;
then B2 c= the carrier of L1 by A2,A7,XBOOLE_1:1;
then reconsider B1=B2 as Subset of L1;
ex_inf_of B2,L2 by YELLOW_0:17;
then inf B1 = inf B2 by A1,YELLOW_0:27;
hence thesis by A2,A7;
end;
then A8:Y1 = Y2 by A5,XBOOLE_0:def 10;
ex_sup_of Y1,L1 by YELLOW_0:17;
hence thesis by A1,A3,A4,A8,YELLOW_0:26;
end;
definition
let L be non empty TopRelStr;
attr L is lim-inf means:
Def2:
the topology of L = xi L;
end;
definition
cluster lim-inf -> TopSpace-like (non empty TopRelStr);
coherence
proof
let L be non empty TopRelStr;
assume A1:L is lim-inf;
set T = ConvergenceSpace lim_inf-Convergence L;
A2:the topology of L = xi L by A1,Def2 .= the topology of T by WAYBEL28:def 4;
the carrier of L = the carrier of T by YELLOW_6:def 27;
then A3:the carrier of L in the topology of L by A2,PRE_TOPC:def 1;
A4:(for a being Subset-Family of L st a c= the topology of L
holds (union a) in the topology of L)
proof
let a being Subset-Family of L;
assume A5:a c= the topology of L;
reconsider b = a as Subset-Family of T by YELLOW_6:def 27;
(union b) in the topology of T by A2,A5,PRE_TOPC:def 1;
hence (union a) in the topology of L by A2;
end;
(for a,b being Subset of L st
a in the topology of L & b in the topology of L
holds a /\ b in the topology of L) by A2,PRE_TOPC:def 1;
hence thesis by A3,A4,PRE_TOPC:def 1;
end;
end;
definition
cluster trivial -> lim-inf TopLattice;
coherence
proof let L be TopLattice;
assume L is trivial;
then reconsider L' = L as trivial TopLattice;
consider x being Point of L';
the carrier of ConvergenceSpace lim_inf-Convergence L = the carrier of L'
by YELLOW_6:def 27;
then reconsider S = ConvergenceSpace lim_inf-Convergence L as
trivial non empty TopSpace by REALSET1:def 13;
reconsider y = x as Point of S by YELLOW_6:def 27;
thus the topology of L = {{},{y}} by YELLOW_9:9
.= the topology of S by YELLOW_9:9 .= xi L by WAYBEL28:def 4;
end;
end;
definition
cluster lim-inf continuous complete TopLattice;
existence
proof
consider L being trivial non empty TopLattice;
take L; thus thesis;
end;
end;
theorem Th2:
for L1, L2 being non empty 1-sorted
st the carrier of L1 = the carrier of L2
for N1 being NetStr over L1
ex N2 being strict NetStr over L2 st
the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2
proof let L1, L2 be non empty 1-sorted such that
A1: the carrier of L1 = the carrier of L2;
let N1 be NetStr over L1;
reconsider f = the mapping of N1 as
Function of the carrier of N1, the carrier of L2 by A1;
take NetStr(#the carrier of N1, the InternalRel of N1, f#);
thus thesis;
end;
theorem Th3:
for L1, L2 being non empty 1-sorted
st the carrier of L1 = the carrier of L2
for N1 being NetStr over L1 st N1 in NetUniv L1
ex N2 being strict net of L2 st N2 in NetUniv L2 &
the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2
proof let L1, L2 be non empty 1-sorted such that
A1: the carrier of L1 = the carrier of L2;
let N1 be NetStr over L1; assume N1 in NetUniv L1;
then consider N being strict net of L1 such that
A2: N = N1 & the carrier of N in the_universe_of the carrier of L1
by YELLOW_6:def 14;
reconsider f = the mapping of N as
Function of the carrier of N, the carrier of L2 by A1;
take NetStr(#the carrier of N, the InternalRel of N, f#);
thus thesis by A1,A2,YELLOW_6:def 14;
end;
Lm1: now
let L1, L2 be non empty RelStr;
let N1 be net of L1, N2 be net of L2 such that
A1: the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2;
deffunc I1(Element of N1) =
{N1.i where i is Element of N1: i >= $1};
deffunc I2(Element of N2) =
{N2.i where i is Element of N2: i >= $1};
let j1 be Element of N1;
let j2 be Element of N2 such that
A2: j1 = j2;
thus I1(j1) c= I2(j2)
proof let y be set; assume y in I1(j1);
then consider i1 being Element of N1 such that
A3: y = N1.i1 & i1 >= j1;
reconsider i1, j1 as Element of N1;
reconsider i2 = i1, j2 as Element of N2 by A1;
i1 >= j1 by A3;
then A4: i2 >= j2 by A1,A2,YELLOW_0:1;
N1.i1 = (the mapping of N1).i1 by WAYBEL_0:def 8
.= N2.i2 by A1,WAYBEL_0:def 8;
hence thesis by A3,A4;
end;
end;
Lm2: now
let L1, L2 be /\-complete Semilattice such that
A1: the RelStr of L1 = the RelStr of L2;
let N1 be net of L1, N2 be net of L2 such that
A2: the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2;
deffunc I1(Element of N1) =
{N1.i where i is Element of N1: i >= $1};
deffunc I2(Element of N2) =
{N2.i where i is Element of N2: i >= $1};
set U1 =
{"/\"
(I1(j), L1) where j is Element of N1: not contradiction};
set U2 =
{"/\"
(I2(j), L2) where j is Element of N2: not contradiction};
thus U1 c= U2
proof let x; assume x in U1;
then consider j1 being Element of N1 such that
A3: x = "/\"(I1(j1), L1);
reconsider j2 = j1 as Element of N2 by A2;
A4: I1(j1) = I2(j2)
proof
thus I1(j1) c= I2(j2) & I2(j2) c= I1(j1) by A2,Lm1;
end;
reconsider j1 as Element of N1;
[#]N1 = the carrier of N1 & [#]N1 is directed
by PRE_TOPC:12,WAYBEL_0:def 6;
then consider j0 being Element of N1 such that j0 in the carrier of N1 and
A5: j1 <= j0 & j1 <= j0 by WAYBEL_0:def 1;
A6: N1.j0 in I1(j1) by A5;
I1(j1) c= the carrier of L1
proof let x; assume x in I1(j1);
then ex i being Element of N1 st x = N1.i & i >= j1;
hence thesis;
end;
then reconsider S = I1(j1) as non empty Subset of L1 by A6;
ex_inf_of S, L1 by WAYBEL_0:76;
then x = "/\"(I2(j2), L2) by A1,A3,A4,YELLOW_0:27;
hence thesis;
end;
end;
theorem Th4:
for L1, L2 being /\-complete up-complete Semilattice
st the RelStr of L1 = the RelStr of L2
for N1 being net of L1, N2 being net of L2
st the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2
holds lim_inf N1 = lim_inf N2
proof let L1, L2 be /\-complete up-complete Semilattice such that
A1: the RelStr of L1 = the RelStr of L2;
let N1 be net of L1, N2 be net of L2 such that
A2: the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2;
deffunc I1(Element of N1) =
{N1.i where i is Element of N1: i >= $1};
deffunc I2(Element of N2) =
{N2.i where i is Element of N2: i >= $1};
set U1 =
{"/\"
(I1(j), L1) where j is Element of N1: not contradiction};
set U2 =
{"/\"
(I2(j), L2) where j is Element of N2: not contradiction};
A3: lim_inf N1 = "\/"(U1, L1) by WAYBEL11:def 6;
A4: lim_inf N2 = "\/"(U2, L2) by WAYBEL11:def 6;
U1 c= the carrier of L1
proof let x; assume x in U1;
then ex j being Element of N1 st x = "/\"(I1(j), L1);
hence thesis;
end;
then reconsider U1 as Subset of L1;
U1 is non empty directed by WAYBEL32:11;
then A5: ex_sup_of U1, L1 by WAYBEL_0:75;
U1 = U2
proof
thus U1 c= U2 & U2 c= U1 by A1,A2,Lm2;
end;
hence thesis by A1,A3,A4,A5,YELLOW_0:26;
end;
theorem Th5:
for L1, L2 being non empty 1-sorted
st the carrier of L1 = the carrier of L2
for N1 being net of L1, N2 being net of L2
st the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2
for S1 being subnet of N1
ex S2 being strict subnet of N2 st
the RelStr of S1 = the RelStr of S2 &
the mapping of S1 = the mapping of S2
proof let L1, L2 be non empty 1-sorted such that
A1: the carrier of L1 = the carrier of L2;
let N1 be net of L1, N2 be net of L2 such that
A2: the RelStr of N1 = the RelStr of N2 and
A3: the mapping of N1 = the mapping of N2;
let S1 be subnet of N1;
consider S2 being strict NetStr over L2 such that
A4: the RelStr of S1 = the RelStr of S2 and
A5: the mapping of S1 = the mapping of S2 by A1,Th2;
consider f being map of S1, N1 such that
A6: the mapping of S1 = (the mapping of N1)*f and
A7: for B5 being Element of N1 holds
ex B6 being Element of S1 st
for B7 being Element of S1 st B6 <= B7 holds B5 <= f.B7
by YELLOW_6:def 12;
[#]S1 = the carrier of S1 & [#]S2 = the carrier of S2 &
[#]S1 is directed by PRE_TOPC:12,WAYBEL_0:def 6;
then [#]S2 is directed by A4,WAYBEL_0:3;
then reconsider S2 as strict net of L2
by A4,STRUCT_0:def 1,WAYBEL_0:def 6,WAYBEL_8:13;
reconsider g = f as map of S2, N2 by A2,A4;
S2 is subnet of N2
proof take g;
thus the mapping of S2 = (the mapping of N2)*g by A3,A5,A6;
let B2 be Element of N2;
reconsider b2 = B2 as Element of N1 by A2;
consider b6 being Element of S1 such that
A8: for b7 being Element of S1 st b6 <= b7 holds b2 <= f.b7 by A7;
reconsider B3 = b6 as Element of S2 by A4;
take B3; let B4 be Element of S2;
reconsider b4 = B4 as Element of S1 by A4;
assume B3 <= B4;
then b6 <= b4 by A4,YELLOW_0:1;
then b2 <= f.b4 by A8;
hence B2 <= g.B4 by A2,YELLOW_0:1;
end;
hence thesis by A4,A5;
end;
theorem Th6:
for L1, L2 being /\-complete up-complete Semilattice
st the RelStr of L1 = the RelStr of L2
for N1 being NetStr over L1, a being set st [N1,a] in lim_inf-Convergence L1
ex N2 being strict net of L2 st [N2,a] in lim_inf-Convergence L2 &
the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2
proof let L1, L2 be /\-complete up-complete Semilattice such that
A1: the RelStr of L1 = the RelStr of L2;
let N1 be NetStr over L1, a be set; assume
A2: [N1,a] in lim_inf-Convergence L1;
lim_inf-Convergence L1 c= [:NetUniv L1, the carrier of L1:]
by YELLOW_6:def 21;
then consider N, x being set such that
A3: N in NetUniv L1 & x in the carrier of L1 & [N1,a] = [N,x]
by A2,ZFMISC_1:def 2;
reconsider x as Element of L1 by A3;
A4: N = N1 & x = a by A3,ZFMISC_1:33;
then consider N2 being strict net of L2 such that
A5: N2 in NetUniv L2 &
the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2 by A1,A3,Th3;
take N2;
ex N being strict net of L1 st N = N1 &
the carrier of N in the_universe_of the carrier of L1
by A3,A4,YELLOW_6:def 14;
then reconsider N1 as strict net of L1;
now let M being subnet of N2;
consider M1 being strict subnet of N1 such that
A6: the RelStr of M = the RelStr of M1 &
the mapping of M = the mapping of M1 by A1,A5,Th5;
thus x = lim_inf M1 by A2,A3,A4,WAYBEL28:def 3 .= lim_inf M by A1,A6,Th4;
end;
hence thesis by A1,A4,A5,WAYBEL28:def 3;
end;
theorem Th7:
for L1, L2 being non empty 1-sorted
for N1 being non empty NetStr over L1
for N2 being non empty NetStr over L2
st the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2
for X being set st N1 is_eventually_in X
holds N2 is_eventually_in X
proof let L1, L2 be non empty 1-sorted;
let N1 be non empty NetStr over L1;
let N2 be non empty NetStr over L2 such that
A1: the RelStr of N1 = the RelStr of N2 &
the mapping of N1 = the mapping of N2;
let X be set;
given i1 being Element of N1 such that
A2: for j being Element of N1 st i1 <= j holds N1.j in X;
reconsider i2 = i1 as Element of N2 by A1;
take i2; let j2 be Element of N2;
reconsider j1 = j2 as Element of N1 by A1;
assume i2 <= j2;
then i1 <= j1 by A1,YELLOW_0:1;
then N1.j1 in X by A2;
then (the mapping of N2).j2 in X by A1,WAYBEL_0:def 8;
hence thesis by WAYBEL_0:def 8;
end;
Lm3:
for L1, L2 being /\-complete up-complete Semilattice
st the RelStr of L1 = the RelStr of L2
holds the topology of ConvergenceSpace lim_inf-Convergence L1
c= the topology of ConvergenceSpace lim_inf-Convergence L2
proof let L1, L2 be /\-complete up-complete Semilattice such that
A1: the RelStr of L1 = the RelStr of L2;
let x be set; assume
A2: x in the topology of ConvergenceSpace lim_inf-Convergence L1;
A3: the topology of ConvergenceSpace lim_inf-Convergence L2 =
{ V where V is Subset of L2:
for p being Element of L2 st p in V
for N being net of L2 st [N,p] in
lim_inf-Convergence L2 holds N is_eventually_in V}
by YELLOW_6:def 27;
the topology of ConvergenceSpace lim_inf-Convergence L1 =
{ V where V is Subset of L1:
for p being Element of L1 st p in V
for N being net of L1 st [N,p] in
lim_inf-Convergence L1 holds N is_eventually_in V}
by YELLOW_6:def 27;
then consider V being Subset of L1 such that
A4: x = V and
A5: for p being Element of L1 st p in V
for N being net of L1 st [N,p] in
lim_inf-Convergence L1 holds N is_eventually_in V by A2;
reconsider V2 = V as Subset of L2 by A1;
now let p be Element of L2 such that
A6: p in V2;
let N be net of L2; assume
[N,p] in lim_inf-Convergence L2;
then consider N1 being strict net of L1 such that
A7: [N1,p] in lim_inf-Convergence L1 &
the RelStr of N = the RelStr of N1 &
the mapping of N = the mapping of N1 by A1,Th6;
N1 is_eventually_in V by A5,A6,A7;
hence N is_eventually_in V2 by A7,Th7;
end;
hence thesis by A3,A4;
end;
theorem
for L1, L2 being /\-complete up-complete Semilattice
st the RelStr of L1 = the RelStr of L2
holds ConvergenceSpace lim_inf-Convergence L1
= ConvergenceSpace lim_inf-Convergence L2
proof let L1, L2 be /\-complete up-complete Semilattice such that
A1: the RelStr of L1 = the RelStr of L2;
set C1 = lim_inf-Convergence L1;
set T1 = ConvergenceSpace C1;
set C2 = lim_inf-Convergence L2;
set T2 = ConvergenceSpace C2;
A2: the carrier of T2 = the carrier of L2 by YELLOW_6:def 27;
the topology of T1 = the topology of T2
proof
thus the topology of T1 c= the topology of T2 by A1,Lm3;
thus thesis by A1,Lm3;
end;
hence thesis by A1,A2,YELLOW_6:def 27;
end;
theorem Th9:
for L1, L2 being /\-complete up-complete Semilattice
st the RelStr of L1 = the RelStr of L2
holds xi L1 = xi L2
proof let L1, L2 be /\-complete up-complete Semilattice;
A1: xi L1 = the topology of ConvergenceSpace lim_inf-Convergence L1 &
xi L2 = the topology of ConvergenceSpace lim_inf-Convergence L2
by WAYBEL28:def 4;
assume the RelStr of L1 = the RelStr of L2;
hence xi L1 c= xi L2 & xi L2 c= xi L1 by A1,Lm3;
end;
definition
let R be /\-complete (non empty reflexive RelStr);
cluster -> /\-complete TopAugmentation of R;
coherence
proof let T be TopAugmentation of R;
let X be non empty Subset of T;
A1: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
then reconsider Y = X as non empty Subset of R;
consider x being Element of R such that
A2: x is_<=_than Y and
A3: for y being Element of R st y is_<=_than Y holds x >= y by WAYBEL_0:def 40;
reconsider y = x as Element of T by A1;
take y; thus y is_<=_than X by A1,A2,YELLOW_0:2;
let z be Element of T;
reconsider v = z as Element of R by A1;
assume z is_<=_than X;
then v is_<=_than Y by A1,YELLOW_0:2;
then x >= v by A3;
hence y >= z by A1,YELLOW_0:1;
end;
end;
definition
let R be Semilattice;
cluster -> with_infima TopAugmentation of R;
coherence
proof let T be TopAugmentation of R;
let x,y be Element of T;
A1: the RelStr of T = the RelStr of R by YELLOW_9:def 4;
then reconsider x' = x, y' = y as Element of R;
consider z' being Element of R such that
A2: z' <= x' & z' <= y' and
A3: for v' being Element of R st v' <= x' & v' <= y' holds v' <= z'
by LATTICE3:def 11;
reconsider z = z' as Element of T by A1;
take z; thus z <= x & z <= y by A1,A2,YELLOW_0:1;
let v be Element of T;
reconsider v' = v as Element of R by A1;
assume v <= x & v <= y;
then v' <= x' & v' <= y' by A1,YELLOW_0:1;
then v' <= z' by A3;
hence v <= z by A1,YELLOW_0:1;
end;
end;
definition
let L be /\-complete up-complete Semilattice;
cluster strict lim-inf TopAugmentation of L;
existence
proof set T = TopRelStr(# the carrier of L, the InternalRel of L, xi L #);
A1: the RelStr of T = the RelStr of L;
then reconsider T as TopAugmentation of L by YELLOW_9:def 4;
take T; thus T is strict;
thus the topology of T = xi T by A1,Th9;
end;
end;
theorem Th10:
for L being /\-complete up-complete Semilattice
for X being lim-inf TopAugmentation of L
holds xi L = the topology of X
proof let L be /\-complete up-complete Semilattice;
let X be lim-inf TopAugmentation of L;
the topology of X = xi X &
the RelStr of X = the RelStr of L by Def2,YELLOW_9:def 4;
hence thesis by Th9;
end;
definition
let L be /\-complete up-complete Semilattice;
func Xi L -> strict TopAugmentation of L means:
Def3:
it is lim-inf;
uniqueness
proof let T1, T2 be strict TopAugmentation of L such that
A1: the topology of T1 = xi T1 and
A2: the topology of T2 = xi T2;
the RelStr of T1 = the RelStr of L & the RelStr of T2 = the RelStr of L
by YELLOW_9:def 4;
hence thesis by A1,A2,Th9;
end;
existence
proof set T = TopRelStr(#the carrier of L, the InternalRel of L, xi L#);
A3: the RelStr of T = the RelStr of L;
then reconsider T as strict TopAugmentation of L by YELLOW_9:def 4;
take T; thus the topology of T = xi T by A3,Th9;
end;
end;
definition
let L be /\-complete up-complete Semilattice;
cluster Xi L -> lim-inf;
coherence by Def3;
end;
theorem Th11:
for L being complete LATTICE, N being net of L holds
lim_inf N = "\/"({inf (N|i) where i is Element of N: not contradiction}, L)
proof
let L be complete LATTICE, N be net of L;
set X ={"/\"({N.i where i is Element of N:i >= j},L)
where j is Element of N: not contradiction};
set Y ={inf (N|i) where i is Element of N: not contradiction};
A1:lim_inf N = "\/"(X,L) by WAYBEL11:def 6;
for x being set st x in X holds x in Y
proof
let x be set;
assume x in X;
then consider j being Element of N such that
A2: x = "/\"({N.i where i is Element of N : i >= j},L);
set S = {N.i where i is Element of N : i >= j};
reconsider x as Element of L by A2;
A3: ex_inf_of S,L by YELLOW_0:17;
then A4: S is_>=_than x &
for a being Element of L st S is_>=_than a holds a <= x
by A2,YELLOW_0:def 10;
reconsider i=j as Element of N;
A5: ex_inf_of rng the mapping of (N|i),L by YELLOW_0:17;
for b being set st b in rng the mapping of (N|i) holds b in S
proof
let b being set;
assume b in rng the mapping of (N|i);
then b in {(N|i).k where k is Element of N|i:not
contradiction}
by WAYBEL11:19;
then consider k being Element of N|i such that
A6: b = (N|i).k;
the carrier of N|i c= the carrier of N by WAYBEL_9:13;
then k in the carrier of N by TARSKI:def 3;
then reconsider l = k as Element of N;
k in the carrier of N|i;
then k in { y where y is Element of N : i <= y} by WAYBEL_9:12;
then consider y being Element of N such that
A7: k = y & i <= y;
reconsider k as Element of N|i;
N.l = (N|i).k by WAYBEL_9:16;
hence thesis by A6,A7;
end;
then A8: rng the mapping of (N|i) c= S by TARSKI:def 3;
for b being set st b in S holds b in rng the mapping of (N|i)
proof
let b being set;
assume b in S;
then consider k being Element of N such that
A9: b = N.k & k >= j;
reconsider l = k as Element of N;
l in { y where y is Element of N : i <= y} by A9;
then reconsider k as Element of N|i by WAYBEL_9:12;
reconsider k as Element of N|i;
N.l = (N|i).k by WAYBEL_9:16;
then b in {(N|i).m where m is Element of N|i:not
contradiction}
by A9;
hence thesis by WAYBEL11:19;
end;
then S c= rng the mapping of (N|i) by TARSKI:def 3;
then A10: S = rng the mapping of (N|i) by A8,XBOOLE_0:def 10;
A11: rng the mapping of (N|i) is_>=_than x
proof let b being Element of L;
thus thesis by A4,A8,LATTICE3:def 8;
end;
for a being Element of L st rng the mapping of (N|i) is_>=_than a
holds a <= x by A2,A3,A10,YELLOW_0:def 10;
then consider i being Element of N such that
A12: ex_inf_of rng the mapping of (N|i),L &
rng the mapping of (N|i) is_>=_than x &
for a being Element of L st
rng the mapping of (N|i) is_>=_than a holds a <= x by A5,A11;
A13: x = "/\"(rng the mapping of (N|i),L) by A12,YELLOW_0:def 10;
inf (N|i) = Inf the mapping of (N|i) by WAYBEL_9:def 2
.= "/\"(rng the mapping of (N|i),L) by YELLOW_2:def 6;
hence thesis by A13;
end;
then A14:X c= Y by TARSKI:def 3;
for x being set st x in Y holds x in X
proof
let x being set;
assume x in Y;
then consider i being Element of N such that
A15: x = inf (N|i);
reconsider x as Element of L by A15;
A16: x = Inf the mapping of (N|i) by A15,WAYBEL_9:def 2
.= "/\"(rng the mapping of (N|i),L) by YELLOW_2:def 6;
set S = {N.j where j is Element of N : j >= i};
rng the mapping of (N|i) = S
proof
for b being set st b in rng the mapping of (N|i) holds b in S
proof
let b being set;
assume b in rng the mapping of (N|i);
then b in {(N|i).k where k is Element of N|i:not
contradiction}
by WAYBEL11:19;
then consider k being Element of N|i such that
A17: b = (N|i).k;
the carrier of N|i c= the carrier of N by WAYBEL_9:13;
then k in the carrier of N by TARSKI:def 3;
then reconsider l = k as Element of N;
k in the carrier of N|i;
then k in { y where y is Element of N : i <= y} by WAYBEL_9:12;
then consider y being Element of N such that
A18: k = y & i <= y;
reconsider k as Element of N|i;
N.l = (N|i).k by WAYBEL_9:16;
hence thesis by A17,A18;
end;
then A19: rng the mapping of (N|i) c= S by TARSKI:def 3;
for b being set st b in S holds b in rng the mapping of (N|i)
proof
let b being set;
assume b in S;
then consider k being Element of N such that
A20: b = N.k & k >= i;
reconsider l = k as Element of N;
l in { y where y is Element of N : i <= y} by A20;
then reconsider k as Element of N|i by WAYBEL_9:12;
reconsider k as Element of N|i;
N.l = (N|i).k by WAYBEL_9:16;
then b in {(N|i).m where m is Element of N|i:not
contradiction}
by A20;
hence thesis by WAYBEL11:19;
end;
then S c= rng the mapping of (N|i) by TARSKI:def 3;
hence thesis by A19,XBOOLE_0:def 10;
end;
hence thesis by A16;
end;
then Y c= X by TARSKI:def 3;
hence thesis by A1,A14,XBOOLE_0:def 10;
end;
theorem Th12:
for L being complete LATTICE,
F being proper Filter of BoolePoset [#]L,
f being Subset of L st f in F
for i being Element of a_net F st i`2 = f
holds inf f = inf ((a_net F)|i)
proof
let L be complete LATTICE;
let F be proper Filter of BoolePoset [#]L;
let f be Subset of L;
assume A1: f in F;
let i be Element of a_net F;
assume A2: i`2 = f;
A3:inf ((a_net F)|i) = Inf the mapping of ((a_net F)|i) by WAYBEL_9:def 2
.= "/\"(rng the mapping of ((a_net F)|i),L) by YELLOW_2:def 6;
for b being set st b in rng the mapping of ((a_net F)|i) holds b in f
proof
let b being set;
assume b in rng the mapping of ((a_net F)|i);
then b in {((a_net F)|i).k where k is Element of
the carrier of (a_net F)|i:not contradiction} by WAYBEL11:19;
then consider k being Element of (a_net F)|i such that
A4: b = ((a_net F)|i).k;
the carrier of (a_net F)|i c= the carrier of (a_net F) by WAYBEL_9:13;
then A5: k in the carrier of (a_net F) by TARSKI:def 3;
then reconsider l = k as Element of a_net F;
k in {[c, g] where c is Element of L, g is Element of F: c in g}
by A5,YELLOW19:def 4;
then consider c being Element of L, g being Element of F such that
A6:k = [c,g] & c in g;
A7:k`1 = c & k`2 = g by A6,MCART_1:def 1,def 2;
k in the carrier of (a_net F)|i;
then k in { y where y is Element of a_net F : i <= y} by WAYBEL_9:12;
then consider y being Element of a_net F such that
A8: k = y & i <= y;
A9: l`2 c= f by A2,A8,YELLOW19:def 4;
reconsider k as Element of (a_net F)|i;
(a_net F).l = ((a_net F)|i).k by WAYBEL_9:16;
then b = l`1 by A4,YELLOW19:def 4;
hence thesis by A6,A7,A9;
end;
then A10:rng the mapping of ((a_net F)|i) c= f by TARSKI:def 3;
for b being set st b in f holds b in rng the mapping of ((a_net F)|i)
proof
let b being set;
assume A11:b in f;
then reconsider b as Element of L;
reconsider f as Element of F by A1;
[b,f] in {[a, g] where a is Element of L, g is Element of F: a in g}
by A11;
then [b,f] in the carrier of (a_net F) by YELLOW19:def 4;
then reconsider k = [b,f] as Element of (a_net F)
;
k`2 c= i`2 & k`1 = b by A2,MCART_1:def 1,def 2;
then A12: b = (a_net F).k & i <= k by YELLOW19:def 4;
reconsider l = k as Element of (a_net F);
l in { y where y is Element of (a_net F) : i <= y} by A12;
then reconsider k as Element of (a_net F)|i by WAYBEL_9:12;
reconsider k as Element of (a_net F)|i;
(a_net F).l = ((a_net F)|i).k by WAYBEL_9:16;
then b in {((a_net F)|i).m where m is Element of
the carrier of (a_net F)|i:not contradiction} by A12;
hence thesis by WAYBEL11:19;
end;
then f c= rng the mapping of ((a_net F)|i) by TARSKI:def 3;
hence thesis by A3,A10,XBOOLE_0:def 10;
end;
theorem Th13:
for L being complete LATTICE,
F being proper Filter of BoolePoset [#]L
holds lim_inf F = lim_inf a_net F
proof
let L be complete LATTICE;
let F be proper Filter of BoolePoset [#]L;
set X ={inf ((a_net F)|i) where i is Element of a_net F: not contradiction};
set Y = {inf B where B is Subset of L: B in F};
A1:lim_inf F = "\/"(Y,L) by Def1;
A2:lim_inf a_net F = "\/"(X,L) by Th11;
for x being set st x in X holds x in Y
proof
let x be set;
assume x in X;
then consider i being Element of a_net F such that
A3: x = inf ((a_net F)|i);
reconsider i as Element of a_net F;
i in the carrier of a_net F;
then i in {[b, g] where b is Element of L, g is Element of F: b in g}
by YELLOW19:def 4;
then consider a being Element of L, f being Element of F such that
A4: i = [a,f] & a in f;
reconsider f as Element of BoolePoset [#]L;
f is Element of bool [#]L by WAYBEL_7:4;
then f c= [#]L;
then f c= the carrier of L by PRE_TOPC:12;
then reconsider f as Subset of L;
reconsider i as Element of a_net F;
i`2 = f by A4,MCART_1:def 2;
then inf f = inf ((a_net F)|i) by Th12;
hence thesis by A3;
end;
then A5:X c= Y by TARSKI:def 3;
for x being set st x in Y holds x in X
proof
let x be set;
assume x in Y;
then consider B being Subset of L such that
A6: x = inf B & B in F;
not Bottom (BoolePoset [#]L) in F by WAYBEL_7:8;
then B <> {} by A6,YELLOW_1:18;
then consider a being Element of L such that
A7:a in B by SUBSET_1:10;
reconsider B as Element of F by A6;
reconsider a as Element of L;
[a,B] in {[b,f] where b is Element of L, f is Element of F: b in f}
by A7;
then [a,B] in the carrier of a_net F by YELLOW19:def 4;
then reconsider i = [a,B] as Element of a_net F;
i`2 = B by MCART_1:def 2;
then x = inf ((a_net F)|i) by A6,Th12;
hence thesis;
thus thesis;
end;
then Y c= X by TARSKI:def 3;
hence thesis by A1,A2,A5,XBOOLE_0:def 10;
end;
Lm4:
for L being LATTICE, F being non empty Subset of BoolePoset [#]L holds
{[a, f] where a is Element of L, f is Element of F: a in f} c=
[:the carrier of L, bool the carrier of L:]
proof
let L be LATTICE;
let F be non empty Subset of BoolePoset [#]L;
let x be set;
assume x in {[a, f] where a is Element of L, f is Element of F: a in f};
then consider a being Element of L, f being Element of F such that
A1: x = [a,f] & a in f;
f is Element of bool [#]L by WAYBEL_7:4;
then f is Element of bool the carrier of L by PRE_TOPC:12;
hence thesis by A1,ZFMISC_1:def 2;
end;
theorem Th14:
for L being complete LATTICE,
F being proper Filter of BoolePoset [#]L
holds a_net F in NetUniv L
proof
let L be complete LATTICE;
let F be proper Filter of BoolePoset [#]L;
set S = {[a, f] where a is Element of L, f is Element of F: a in f};
A1:S = the carrier of a_net F by YELLOW19:def 4;
A2:S c= [:the carrier of L, bool the carrier of L:] by Lm4;
set UN = the_universe_of the carrier of L;
A3:UN = Tarski-Class the_transitive-closure_of the carrier of L
by YELLOW_6:def 3;
reconsider UN as universal set;
A4:the_transitive-closure_of the carrier of L in UN by A3,CLASSES1:5;
the carrier of L c= the_transitive-closure_of the carrier of L
by CLASSES1:59;
then A5:the carrier of L in UN by A3,A4,CLASSES1:6;
then bool the carrier of L in UN by CLASSES2:65;
then [:the carrier of L, bool the carrier of L:] in UN by A5,CLASSES2:67;
then S in UN by A2,CLASSES1:def 1;
hence thesis by A1,YELLOW_6:def 14;
end;
theorem Th15:
for L being complete LATTICE,
F being ultra Filter of BoolePoset [#]L
for p being greater_or_equal_to_id map of a_net F, a_net F
holds lim_inf F >= inf ((a_net F) * p)
proof
let L be complete LATTICE,
F be ultra Filter of BoolePoset [#]L,
p be greater_or_equal_to_id map of a_net F, a_net F;
set M = (a_net F)*p;
A1:the carrier of M = the carrier of a_net F by WAYBEL28:7;
then reconsider g = p as map of M, a_net F;
set rM = rng the mapping of M;
consider C being Element of F;
rM c= the carrier of L;
then A2:rM c= [#]L by PRE_TOPC:12;
F c= the carrier of BoolePoset [#]L; then
F c= bool [#]L by WAYBEL_7:4; then
F is Subset of bool [#]L;
then A3: C in bool [#]L by TARSKI:def 3;
then C \ rM c= C & C /\ rM c= C \/ rM & C \/ rM c= [#]L by A2,XBOOLE_1:8,29
;
then A4:C \ rM c= [#]L & C /\ rM c= [#]L by A3,XBOOLE_1:1;
then C \ rM is Element of BoolePoset [#]L &
C /\ rM is Element of BoolePoset [#]L by WAYBEL_7:4;
then reconsider D=C \ rM, A=C /\ rM as Element of BoolePoset [#]
L;
A c= the carrier of L by A4,PRE_TOPC:12;
then reconsider A' = A as Subset of L;
A5:F is prime by WAYBEL_7:26;
A6:D"\/"A = D \/ A by YELLOW_1:17 .= C by XBOOLE_1:51;
now assume
A7: D in F;
consider d being Element of D;
not Bottom (BoolePoset [#]L) in F by WAYBEL_7:8;
then A8: D <> {} by A7,YELLOW_1:18;
then A9: d in D;
D c= the carrier of L by A4,PRE_TOPC:12;
then reconsider d as Element of L by A9;
reconsider D as Element of F by A7;
[d,D] in {[a, f] where a is Element of L, f is Element of F: a in f}
by A8;
then [d,D] in the carrier of a_net F by YELLOW19:def 4;
then reconsider dD= [d,D] as Element of a_net F;
reconsider dD' = dD as Element of M by A1;
ex i being Element of M st
for j being Element of M st j >= i holds g.j >= dD
proof
consider i being Element of M such that
A10: i = dD';
A11: for j being Element of M st j >= i holds g.j >= dD
proof
let j be Element of M; assume
A12: j >= i;
reconsider j'=j as Element of a_net F by WAYBEL28:7;
A13: j' <= g.j by WAYBEL28:def 1;
reconsider j' as Element of a_net F;
reconsider i'=i as Element of a_net F by WAYBEL28:7;
reconsider i' as Element of a_net F;
the RelStr of M = the RelStr of a_net F by WAYBEL28:def 2;
then i' <= j' by A12,YELLOW_0:1;
hence thesis by A10,A13,YELLOW_0:def 2;
end;
take i;
thus thesis by A11;
end;
then consider i being Element of M such that
A14: for j being Element of M st j >= i holds g.j >= dD; :: REVISION in W28
the RelStr of M = the RelStr of a_net F by WAYBEL28:def 2;
then M is reflexive by WAYBEL_8:12;
then i >= i by YELLOW_0:def 1;
then A15: g.i >= dD by A14;
reconsider G = g.i as Element of a_net F;
g.i in the carrier of a_net F;
then g.i in {[a, f] where a is Element of L, f is Element of F: a in f}
by YELLOW19:def 4;
then consider a being Element of L, f being Element of F such that
A16: g.i = [a, f] & a in f;
A17: (g.i)`1 = a & (g.i)`2 = f by A16,MCART_1:def 1,def 2;
(g.i)`2 = (p.i)`2 & dD`2 = D by MCART_1:def 2;
then A18: (p.i)`2 c= D & (p.i)`1 in (p.i)`2 by A15,A16,A17,YELLOW19:def 4;
A19: dom p = the carrier of a_net F by FUNCT_2:67;
M.i = (the mapping of M).i by WAYBEL_0:def 8
.= ((the mapping of a_net F)*p).i by WAYBEL28:def 2
.= (the mapping of a_net F).(p.i) by A1,A19,FUNCT_1:23
.= (a_net F).G by WAYBEL_0:def 8
.= (p.i)`1 by YELLOW19:def 4;
then A20: not M.i in rM by A18,XBOOLE_0:def 4;
(the mapping of M).i in rM by FUNCT_2:6;
hence contradiction by A20,WAYBEL_0:def 8;
end;
then A21:A c= rM & A in F by A5,A6,WAYBEL_7:def 2,XBOOLE_1:17;
inf M = Inf the mapping of M by WAYBEL_9:def 2
.= "/\"(rM,L) by YELLOW_2:def 6;
then A22:inf M <= inf A' by A21,WAYBEL_7:3;
set Y = {inf B where B is Subset of L: B in F};
A23:inf A' in Y by A21;
A24:ex_sup_of Y,L by YELLOW_0:17;
lim_inf F = "\/"(Y,L) by Def1;
then inf A' <= lim_inf F by A23,A24,YELLOW_4:1;
hence thesis by A22,YELLOW_0:def 2;
end;
theorem Th16:
for L being complete LATTICE,
F being ultra Filter of BoolePoset [#]L
holds for M being subnet of a_net F holds lim_inf F = lim_inf M
proof
let L be complete LATTICE,
F be ultra Filter of BoolePoset [#]L,
M be subnet of a_net F;
A1: lim_inf F = lim_inf a_net F by Th13;
for p being greater_or_equal_to_id map of a_net F, a_net F
holds lim_inf F >= inf ((a_net F) * p) by Th15;
hence thesis by A1,WAYBEL28:15;
end;
theorem Th17:
for L being non empty 1-sorted
for N being net of L
for A being set st N is_often_in A
ex N' being strict subnet of N st
rng the mapping of N' c= A & N' is SubNetStr of N
proof
let L be non empty 1-sorted;
let N be net of L;
let A be set such that A1:N is_often_in A;
reconsider N' = N"A as strict subnet of N by A1,YELLOW_6:31;
A2:rng the mapping of N' c= A
proof
let y be set; assume y in rng the mapping of N';
then consider x being set such that
A3: x in dom the mapping of N' & y = (the mapping of N').x by FUNCT_1:def 5;
A4: x in dom ((the mapping of N)|the carrier of N') by A3,YELLOW_6:def 8;
then x in (dom the mapping of N) /\ the carrier of N' by FUNCT_1:68;
then A5: x in dom the mapping of N & x in the carrier of N' by XBOOLE_0:def 3;
y = ((the mapping of N)|the carrier of N').x by A3,YELLOW_6:def 8;
then A6: y = (the mapping of N).x by A4,FUNCT_1:68;
x in (the mapping of N)"A by A5,YELLOW_6:def 13;
hence thesis by A6,FUNCT_1:def 13;
end;
take N';
thus thesis by A2;
end;
theorem Th18: :: III. 3.4. LEMMA, p. 168(?)
for L being complete lim-inf TopLattice, A being non empty Subset of L holds
A is closed iff
for F being ultra Filter of BoolePoset [#]L st A in F holds lim_inf F in A
proof
let L be complete lim-inf TopLattice;
let A be non empty Subset of L;
A1:the topology of L = xi L by Def2;
xi L = the topology of ConvergenceSpace lim_inf-Convergence L
by WAYBEL28:def 4;
then A2:xi L = { V where V is Subset of L:
for p being Element of L st p in V
for N being net of L st [N,p] in lim_inf-Convergence L
holds N is_eventually_in V} by YELLOW_6:def 27;
hereby assume A is closed;
then A` is open by WAYBEL12:def 1;
then A` in xi L by A1,PRE_TOPC:def 5;
then consider V being Subset of L such that
A3: V = A` and
A4: for p being Element of L st p in V
for N being net of L st [N,p] in lim_inf-Convergence L
holds N is_eventually_in V by A2;
let F be ultra Filter of BoolePoset [#]L;
A5: for M being subnet of a_net F holds lim_inf F = lim_inf M by Th16;
a_net F in NetUniv L & lim_inf F = lim_inf a_net F by Th13,Th14;
then A6: [a_net F, lim_inf F] in lim_inf-Convergence L by A5,WAYBEL28:def 3;
assume
A7: A in F;
assume not lim_inf F in A;
then lim_inf F in A` by YELLOW_6:10;
then a_net F is_eventually_in A` by A3,A4,A6;
then consider i being Element of a_net F such that
A8: for j being Element of a_net F st i <= j holds (a_net F).j in A`
by WAYBEL_0:def 11;
A9: the carrier of a_net F =
{[a, f] where a is Element of L, f is Element of F: a in f}
by YELLOW19:def 4;
i in the carrier of a_net F;
then consider a being Element of L, f being Element of F such that
A10: i = [a, f] & a in f by A9;
A is Element of F by A7;
then reconsider A' = A, f' = f as Element of BoolePoset [#]L;
consider B being Element of BoolePoset [#]L such that
A11: B in F & A' >= B & f' >= B by A7,WAYBEL_0:def 2;
consider b being Element of B;
not Bottom (BoolePoset [#]L) in F by WAYBEL_7:8;
then A12:B is non empty by A11,YELLOW_1:18;
then A13: b in B;
the carrier of BoolePoset [#]L = bool [#]L by WAYBEL_7:4
.= bool the carrier of L by PRE_TOPC:12;
then b is Element of L by A13;
then [b, B] in the carrier of a_net F by A9,A11,A12;
then reconsider j = [b, B] as Element of a_net F;
A14: B c= f & B c= A by A11,YELLOW_1:2;
then j`2 c= f by MCART_1:7;
then j`2 c= i`2 by A10,MCART_1:7;
then j >= i by YELLOW19:def 4;
then (a_net F).j in A` by A8;
then j`1 in A` by YELLOW19:def 4;
then b in A` & b in A by A13,A14,MCART_1:7;
hence contradiction by YELLOW_6:10;
end;
assume
A15:for F being ultra Filter of BoolePoset [#]L st A in F holds lim_inf F in A;
set V = A`;
now let p be Element of L such that
A16: p in V;
reconsider x = p as Element of L;
let N be net of L such that
A17: [N,p] in lim_inf-Convergence L;
A` = [#]L \ A by PRE_TOPC:17;
then A18: A` = (the carrier of L)\ A by PRE_TOPC:12;
assume not N is_eventually_in V;
then N is_often_in A by A18,WAYBEL_0:10;
then consider N' being strict subnet of N such that
A19: rng the mapping of N' c= A & N' is SubNetStr of N by Th17;
lim_inf-Convergence L c= [:NetUniv L, the carrier of L:]
by YELLOW_6:def 21;
then A20: N in NetUniv L by A17,ZFMISC_1:106;
A21: the carrier of N' c= the carrier of N by A19,YELLOW_6:19;
consider N1 being strict net of L such that
A22: N1 = N and
A23:the carrier of N1 in the_universe_of the carrier of L
by A20,YELLOW_6:def 14;
the carrier of N' in the_universe_of the carrier of L
by A21,A22,A23,CLASSES1:def 1;
then A24: N' in NetUniv L by YELLOW_6:def 14;
A25: x = lim_inf N' by A17,A20,WAYBEL28:def 3;
now let M be subnet of N';
M is subnet of N by YELLOW_6:24;
hence x = lim_inf M by A17,A20,WAYBEL28:def 3;
end;
then A26: for M being subnet of N' st M in NetUniv L holds x = lim_inf M;
set G = {rng the mapping of N'|j where j is Element of N':
not contradiction};
consider j2 being Element of N';
set g = rng the mapping of N'|j2;
A27:g in G;
for g being set st g in G holds g in the carrier of BoolePoset [#]L
proof
let g be set; assume
g in G;
then consider j3 being Element of N' such that
A28: g = rng the mapping of N'|j3;
g = rng ((the mapping of N')|the carrier of N'|j3)
by A28,WAYBEL_9:def 7;
then g c= rng the mapping of N' by FUNCT_1:76;
then A29: g c= A by A19,XBOOLE_1:1;
A in bool the carrier of L;
then A in bool [#]L by PRE_TOPC:12;
then g c= [#]L by A29,XBOOLE_1:1;
then g in bool [#]L;
hence thesis by WAYBEL_7:4;
end;
then G c= the carrier of BoolePoset [#]L by TARSKI:def 3;
then reconsider G as non empty Subset of BoolePoset [#]L by A27;
A30: not {} in fininfs G
proof
assume {} in fininfs G;
then {} in {"/\"(Y,BoolePoset [#]L) where Y is finite Subset of G:
ex_inf_of Y, BoolePoset [#]L} by WAYBEL_0:def 28;
then consider Y being finite Subset of G such that
A31: {} = "/\"(Y,BoolePoset [#]L) & ex_inf_of Y, BoolePoset [#]L;
Y c= the carrier of BoolePoset [#]L by XBOOLE_1:1;
then reconsider Y as finite Subset of BoolePoset [#]L;
A32: "/\"({},BoolePoset [#]L) = Top BoolePoset [#]L by YELLOW_0:def 12
.= [#]L by YELLOW_1:19;
defpred P[set,set] means ex j being Element of N' st
j = $2 & $1 = rng the mapping of N'|j;
A33: for x being set st x in Y
ex y being set st y in the carrier of N' & P[x,y]
proof
let x be set; assume
A34: x in Y;
assume
A35: for y being set st y in the carrier of N' holds not P[x,y];
x in G by A34;
then consider j being Element of N' such that
A36: x = rng the mapping of N'|j;
thus contradiction by A35,A36;
end;
consider f being Function such that
A37: dom f = Y & rng f c= the carrier of N' and
A38: for x being set st x in Y holds P[x,f.x]
from NonUniqBoundFuncEx(A33);
reconsider C = rng f as finite Subset of [#]N'
by A37,FINSET_1:26,PRE_TOPC:12;
[#]N' is directed by WAYBEL_0:def 6;
then consider j0 being Element of N' such that
A39: j0 in [#]N' & j0 is_>=_than C by WAYBEL_0:1;
for y being set st y in Y holds rng the mapping of N'|j0 c= y
proof
let y be set such that
A40: y in Y;
A41: f.y in rng f by A37,A40,FUNCT_1:12;
then reconsider f1=f.y as Element of N' by A37;
A42: f1 <= j0 by A39,A41,LATTICE3:def 9;
consider j1 being Element of N' such that
A43: j1 = f.y & y = rng the mapping of N'|j1 by A38,A40;
for p being set st p in rng the mapping of N'|j0 holds p in y
proof
let p be set such that
A44: p in rng the mapping of N'|j0;
p in rng ((the mapping of N')|the carrier of N'|j0)
by A44,WAYBEL_9:def 7;
then consider q be set such that
A45: q in dom ((the mapping of N')|the carrier of N'|j0) &
p = ((the mapping of N')|the carrier of N'|j0).q by FUNCT_1:def 5;
q in (dom the mapping of N') /\ the carrier of N'|j0
by A45,FUNCT_1:68;
then A46: q in dom the mapping of N' & q in the carrier of N'|j0
by XBOOLE_0:def 3;
then q in { n' where n' is Element of N' : j0 <=n' } by WAYBEL_9:12;
then consider n' being Element of N' such that
A47: q = n' & j0 <= n';
A48: p = (the mapping of N').q by A45,FUNCT_1:68;
f1 <= n' by A42,A47,YELLOW_0:def 2;
then q in { m' where m' is Element of N' : j1 <=m' } by A43,A47;
then q in the carrier of N'|j1 by WAYBEL_9:12;
then q in (dom the mapping of N') /\ the carrier of N'|j1
by A46,XBOOLE_0:def 3;
then A49: q in dom ((the mapping of N')|the carrier of N'|j1) by FUNCT_1:68;
then p = ((the mapping of N')|the carrier of N'|j1).q by A48,FUNCT_1:68
;
then p in rng((the mapping of N')|the carrier of N'|j1) by A49,FUNCT_1:
12;
hence thesis by A43,WAYBEL_9:def 7;
end;
hence thesis by TARSKI:def 3;
end;
then rng the mapping of N'|j0 c= meet Y by A31,A32,SETFAM_1:6;
then rng the mapping of N'|j0 c= {} by A31,A32,YELLOW_1:20;
hence contradiction by XBOOLE_1:3;
end;
for y being Element of BoolePoset [#]L st (Bottom BoolePoset [#]L) >= y
holds not y in fininfs G
proof
let y be Element of BoolePoset [#]L such that
A50: (Bottom BoolePoset [#]L) >= y;
A51: {} = Bottom BoolePoset [#]L by YELLOW_1:18;
y c= Bottom BoolePoset [#]L by A50,YELLOW_1:2;
hence thesis by A30,A51,XBOOLE_1:3;
end;
then not Bottom BoolePoset [#]L in uparrow fininfs G by WAYBEL_0:def 16;
then uparrow fininfs G is proper by WAYBEL_7:8;
then consider F being Filter of BoolePoset [#]L such that
A52: uparrow fininfs G c= F & F is ultra by WAYBEL_7:30;
consider j0 being Element of N';
A in bool the carrier of L;
then A in bool [#]L by PRE_TOPC:12;
then A53: A in the carrier of BoolePoset [#]L by WAYBEL_7:4;
A54: rng the mapping of N'|j0 in G;
then reconsider rj = rng the mapping of N'|j0,
a = A as Element of BoolePoset [#]L
by A53;
A55: G c= fininfs G & fininfs G c= uparrow fininfs G by WAYBEL_0:16,50;
now let p be set such that
A56: p in rj;
p in rng ((the mapping of N')|the carrier of N'|j0)
by A56,WAYBEL_9:def 7;
then consider q be set such that
A57: q in dom ((the mapping of N')|the carrier of N'|j0) &
p = ((the mapping of N')|the carrier of N'|j0).q by FUNCT_1:def 5;
q in (dom the mapping of N') /\ the carrier of N'|j0
by A57,FUNCT_1:68;
then A58: q in dom the mapping of N' & q in the carrier of N'|j0 by XBOOLE_0:
def 3;
p = (the mapping of N').q by A57,FUNCT_1:68;
hence p in rng the mapping of N' by A58,FUNCT_1:12;
end;
then rj c= rng the mapping of N' by TARSKI:def 3;
then rj c= a by A19,XBOOLE_1:1;
then rj <= a by YELLOW_1:2;
then A59: a in uparrow fininfs G by A54,A55,WAYBEL_0:def 16;
A60: x = "\/"({inf (N'|j) where j is Element of N': not contradiction}, L)
by A25,Th11;
A61: lim_inf F = "\/"({inf f where f is Subset of L: f in F}, L) by Def1;
A62: ex_sup_of {inf f where f is Subset of L: f in F}, L &
ex_sup_of {inf (N'|j) where j is Element of N': not contradiction}, L
by YELLOW_0:17;
{inf (N'|j) where j is Element of N': not contradiction} c=
{inf f where f is Subset of L: f in F}
proof
let x be set such that
A63: x in {inf (N'|j) where j is Element of N': not contradiction};
consider j3 being Element of N' such that
A64: x = inf (N'|j3) by A63;
A65: x = Inf the mapping of (N'|j3) by A64,WAYBEL_9:def 2
.= "/\"(rng the mapping of (N'|j3),L) by YELLOW_2:def 6;
reconsider f1 = rng the mapping of (N'|j3) as Subset of L;
fininfs G c= F by A52,A55,XBOOLE_1:1;
then f1 in G & G c= F by A55,XBOOLE_1:1;
hence thesis by A65;
end; then
A66: x <= lim_inf F by A60,A61,A62,YELLOW_0:34;
{inf f where f is Subset of L: f in F} is_<=_than x
proof
let y be Element of L;
assume y in {inf f where f is Subset of L: f in F};
then consider f0 being Subset of L such that
A67: y = inf f0 & f0 in F;
defpred P[Element of N',Element of N'] means $1 <= $2 & N'.$2 in f0;
A68: now let j be Element of N';
G c= uparrow fininfs G by A55,XBOOLE_1:1; then G
c= F & rng the mapping of N'|j in G by A52,XBOOLE_1:1; then
A69: f0 /\ rng the mapping of N'|j in F by A67,WAYBEL_7:13;
F is ultra Filter of BoolePoset [#]L by A52;
then not Bottom (BoolePoset [#]L) in F by WAYBEL_7:8;
then not {} in F by YELLOW_1:18;
then consider nj being Element of L such that
A70: nj in f0 /\ rng the mapping of N'|j by A69,SUBSET_1:10;
nj in f0 & nj in rng the mapping of N'|j by A70,XBOOLE_0:def 3;
then consider pj' being set such that
A71: pj' in dom the mapping of N'|j & nj=(the mapping of N'|j).pj'
by FUNCT_1:def 5;
pj' in the carrier of (N'|j) by A71;
then pj' in { y' where y' is Element of N' : j <= y' } by WAYBEL_9:12;
then consider pj being Element of N' such that
A72: pj = pj' & j <= pj;
reconsider pj' as Element of (N'|j) by A71;
A73: N'.pj = (N'|j).pj' by A72,WAYBEL_9:16
.=(the mapping of N'|j).pj' by WAYBEL_0:def 8;
take pj;
thus P[j,pj] by A70,A71,A72,A73,XBOOLE_0:def 3;
end;
consider p being map of N', N' such that
A74: for j being Element of N' holds P[j,p.j] from NonUniqExMD(A68);
A75: for M being subnet of N' st M in NetUniv L holds x >= inf M
by A24,A26,WAYBEL28:3;
for j being Element of N' holds j <= p.j by A74;
then p is greater_or_equal_to_id by WAYBEL28:def 1;
then A76: inf (N'*p) <= x by A24,A25,A75,WAYBEL28:14;
for b being set st b in rng the mapping of (N'*p) holds b in f0
proof
let b be set; assume
b in rng the mapping of (N'*p);
then b in {(N'*p).k where k is Element of N'*p
: not contradiction}
by WAYBEL11:19;
then consider k being Element of N'*p such that
A77: b = (N'*p).k;
A78: the carrier of N'*p = the carrier of N' by WAYBEL28:7;
then reconsider l = k as Element of N';
k in the carrier of N' by A78;
then A79: k in dom p by FUNCT_2:67;
(N'*p).k = (the mapping of N'*p).k by WAYBEL_0:def 8
.= ((the mapping of N')*p).k by WAYBEL28:def 2
.= (the mapping of N').(p.k) by A79,FUNCT_1:23
.= N'.(p.l) by WAYBEL_0:def 8;
hence thesis by A74,A77;
end;
then rng the mapping of (N'*p) c= f0 by TARSKI:def 3;
then A80: "/\"(f0,L) <= "/\"(rng the mapping of (N'*p),L) by WAYBEL_7:3;
inf (N'*p) = Inf the mapping of N'*p by WAYBEL_9:def 2
.= "/\"(rng the mapping of (N'*p),L) by YELLOW_2:def 6;
hence thesis by A67,A76,A80,YELLOW_0:def 2;
end;
then lim_inf F <= x by A61,YELLOW_0:32;
then A81: x = lim_inf F by A66,YELLOW_0:def 3;
not p in V` by A16,YELLOW_6:10;
hence contradiction by A15,A52,A59,A81;
end;
then A` in xi L by A2;
then A` is open by A1,PRE_TOPC:def 5;
hence A is closed by WAYBEL12:def 1;
end;
theorem Th19:
for L being non empty reflexive RelStr holds sigma L c= xi L
proof let L be non empty reflexive RelStr;
let x be set; assume
x in sigma L;
hence thesis by WAYBEL28:29;
end;
theorem Th20:
for T1, T2 being non empty TopSpace, B being prebasis of T1
st B c= the topology of T2 &
the carrier of T1 in the topology of T2
holds the topology of T1 c= the topology of T2
proof let T1, T2 be non empty TopSpace;
let B be prebasis of T1 such that
A1: B c= the topology of T2 &
the carrier of T1 in the topology of T2;
FinMeetCl B is Basis of T1 by YELLOW_9:23;
then A2: the topology of T1 = UniCl FinMeetCl B by YELLOW_9:22;
let x be set; assume x in the topology of T1;
then consider Y being Subset-Family of T1 such that
A3: Y c= FinMeetCl B & x = union Y by A2,CANTOR_1:def 1;
A4: Y c= the topology of T2
proof let y be set; assume y in Y;
then consider Z being Subset-Family of T1 such that
A5: Z c= B & Z is finite & y = Intersect Z by A3,CANTOR_1:def 4;
Z c= the topology of T2 by A1,A5,XBOOLE_1:1;
then Z c= bool the carrier of T2 by XBOOLE_1:1;
then reconsider Z' = Z as Subset-Family of T2
by SETFAM_1:def 7;
Z = {} or Z <> {};
then y = the carrier of T1 or Z' c= the topology of T2 &
y = meet Z' & meet Z' = Intersect Z'
by A1,A5,CANTOR_1:def 3,XBOOLE_1:1;
then y = the carrier of T1 or y in FinMeetCl the topology of T2
by A5,CANTOR_1:def 4;
hence thesis by A1,CANTOR_1:5;
end;
then Y c= bool the carrier of T2 by XBOOLE_1:1;
then reconsider Y as Subset-Family of T2 by SETFAM_1:def 7;
union Y in UniCl the topology of T2 by A4,CANTOR_1:def 1;
hence thesis by A3,CANTOR_1:6;
end;
theorem Th21:
for L being complete LATTICE holds omega L c= xi L
proof let L be complete LATTICE;
consider S being lower correct TopAugmentation of L;
consider X being lim-inf TopAugmentation of L;
A1: the RelStr of S = the RelStr of L & the RelStr of X = the RelStr of L
by YELLOW_9:def 4;
reconsider B = {(uparrow x)` where x is Element of S: not contradiction}
as prebasis of S by WAYBEL19:def 1;
A2: the carrier of S in the topology of X by A1,PRE_TOPC:def 1;
B c= the topology of X
proof let b be set; assume b in B;
then consider x being Element of S such that
A3: b = (uparrow x)`;
reconsider y = x as Element of X by A1;
S is SubRelStr of S by YELLOW_6:15;
then X is SubRelStr of S by A1,WAYBEL21:12;
then A4: uparrow y c= uparrow x by WAYBEL23:14;
X is SubRelStr of X by YELLOW_6:15;
then S is SubRelStr of X by A1,WAYBEL21:12;
then uparrow x c= uparrow y by WAYBEL23:14;
then A5: uparrow y = uparrow x by A4,XBOOLE_0:def 10;
A6: b = [#]S \ (uparrow x) by A3,PRE_TOPC:17
.= (the carrier of S) \ uparrow x by PRE_TOPC:12;
set A = uparrow y;
A7: A` = [#]X \ A by PRE_TOPC:17 .= (the carrier of X)\A by PRE_TOPC:12;
A8: inf A = y by WAYBEL_0:39;
now let F be ultra Filter of BoolePoset [#]X;
assume A in F;
then inf A in {inf C where C is Subset of X: C in F};
then inf A <= "\/"({inf C where C is Subset of X: C in F}, X)
by YELLOW_2:24;
then inf A <= lim_inf F by Def1;
hence lim_inf F in A by A8,WAYBEL_0:18;
end;
then A is closed by Th18;
then A` is open by WAYBEL12:def 1;
hence thesis by A1,A5,A6,A7,PRE_TOPC:def 5;
end;
then the topology of S c= the topology of X by A2,Th20;
then omega L c= the topology of X by WAYBEL19:def 2;
hence thesis by Th10;
end;
theorem Th22:
for T1,T2 being TopSpace, T being non empty TopSpace
st T is TopExtension of T1 & T is TopExtension of T2
for R being Refinement of T1,T2
holds T is TopExtension of R
proof let T1,T2 be TopSpace, T be non empty TopSpace such that
A1: the carrier of T1 = the carrier of T and
A2: the topology of T1 c= the topology of T and
A3: the carrier of T2 = the carrier of T and
A4: the topology of T2 c= the topology of T;
let R be Refinement of T1, T2;
A5: the carrier of R = (the carrier of T) \/ (the carrier of T) &
(the topology of T1) \/ (the topology of T2) is prebasis of R
by A1,A3,YELLOW_9:def 6;
hence
the carrier of R = the carrier of T;
reconsider S = (the topology of T1) \/ (the topology of T2)
as prebasis of R by YELLOW_9:def 6;
FinMeetCl S is Basis of R by YELLOW_9:23;
then A6: UniCl FinMeetCl S = the topology of R by YELLOW_9:22;
S c= the topology of T by A2,A4,XBOOLE_1:8;
then FinMeetCl S c= FinMeetCl the topology of T
by A5,CANTOR_1:16;
then the topology of R c= UniCl FinMeetCl the topology of T
by A5,A6,CANTOR_1:9;
hence the topology of R c= the topology of T
by CANTOR_1:7;
end;
theorem Th23:
for T1 being TopSpace, T2 being TopExtension of T1
for A being Subset of T1 holds
(A is open implies A is open Subset of T2) &
(A is closed implies A is closed Subset of T2)
proof let T1 be TopSpace, T2 be TopExtension of T1;
A1: the topology of T1 c= the topology of T2 by YELLOW_9:def 5;
let A be Subset of T1;
thus A is open implies A is open Subset of T2
proof assume A in the topology of T1;
then A in the topology of T2 by A1;
hence thesis by PRE_TOPC:def 5;
end;
A2: the carrier of T1 = the carrier of T2 by YELLOW_9:def 5;
then reconsider B = A as Subset of T2;
A3: [#]T1 = the carrier of T1 & [#]T2 = the carrier of T2 by PRE_TOPC:12;
then reconsider C = [#]T2 \ B as Subset of T2;
assume [#]T1 \ A in the topology of T1;
then C is open by A1,A2,A3,PRE_TOPC:def 5;
hence thesis by PRE_TOPC:def 6;
end;
theorem Th24: :: III. 3.5. LEMMA, p. 168(?)
for L being complete LATTICE holds lambda L c= xi L
proof let L be complete LATTICE;
consider T being Lawson correct TopAugmentation of L;
consider S being Scott TopAugmentation of L;
consider LL being lower correct TopAugmentation of L;
consider LI being lim-inf TopAugmentation of L;
A1: lambda L = the topology of T by WAYBEL19:def 4;
A2: sigma L = the topology of S by YELLOW_9:51;
A3: omega L = the topology of LL by WAYBEL19:def 2;
A4: xi L = the topology of LI by Th10;
A5: the RelStr of T = the RelStr of L &
the RelStr of S = the RelStr of L &
the RelStr of LL = the RelStr of L &
the RelStr of LI = the RelStr of L by YELLOW_9:def 4;
A6: T is Refinement of S,LL by WAYBEL19:29;
the topology of S c= xi L & the topology of LL c= xi L
by A2,A3,Th19,Th21;
then LI is TopExtension of S & LI is TopExtension of LL
by A4,A5,YELLOW_9:def 5;
then LI is TopExtension of T by A6,Th22;
hence thesis by A1,A4,YELLOW_9:def 5;
end;
theorem Th25: :: 3.6. PROPOSITION (B), p. 169(?)
for L being complete LATTICE
for T being lim-inf TopAugmentation of L
for S being Lawson correct TopAugmentation of L
holds T is TopExtension of S
proof let L be complete LATTICE;
let T be lim-inf TopAugmentation of L;
let S be Lawson correct TopAugmentation of L;
A1: lambda L = the topology of S by WAYBEL19:def 4;
A2: the RelStr of T = the RelStr of L &
the RelStr of S = the RelStr of L by YELLOW_9:def 4;
xi L = the topology of T by Th10;
then the topology of S c= the topology of T by A1,Th24;
hence thesis by A2,YELLOW_9:def 5;
end;
theorem Th26:
for L being complete lim-inf TopLattice
for F being ultra Filter of BoolePoset [#]L
holds lim_inf F is_a_convergence_point_of F, L
proof let L be complete lim-inf TopLattice;
let F be ultra Filter of BoolePoset [#]L;
set x = lim_inf F;
A1: [#]L = the carrier of L by PRE_TOPC:12;
let A be Subset of L; assume
A2: A is open & x in A & not A in F;
F is prime by WAYBEL_7:26;
then A3: ([#]L)\A in F by A1,A2,WAYBEL_7:25;
A4: A` = ([#]L)\A & A` = A` by A1,SUBSET_1:def 5;
then A` <> {} & A` is closed by A2,A3,TOPS_1:30,YELLOW19:2;
then x in A` by A3,A4,Th18;
hence contradiction by A2,YELLOW_6:10;
end;
theorem :: 3.6. PROPOSITION (A), p. 169(?)
for L being complete lim-inf TopLattice
holds L is compact being_T1
proof let L be complete lim-inf TopLattice;
now let F be ultra Filter of BoolePoset [#]L;
reconsider x = lim_inf F as Point of L;
take x; thus x is_a_convergence_point_of F, L by Th26;
end;
hence L is compact by YELLOW19:33;
consider T being Lawson correct TopAugmentation of L;
now let x be Point of L;
reconsider y = x as Element of L;
the RelStr of L = the RelStr of T by YELLOW_9:def 4;
then reconsider z = y as Element of T;
L is TopAugmentation of L by YELLOW_9:44;
then L is TopExtension of T & {z} is closed by Th25;
then {y} is closed by Th23;
hence Cl {x} = {x} by PRE_TOPC:52;
end;
hence thesis by FRECHET2:47;
end;