:: Compactness of Lim-inf Topology
:: by Grzegorz Bancerek and Noboru Endou
::
:: 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, ORDERS_2, SUBSET_1, CARD_FIL, YELLOW_1, ORDINAL2,
EQREL_1, REWRITE1, WAYBEL_0, TARSKI, STRUCT_0, ZFMISC_1, WAYBEL_9,
PRE_TOPC, WAYBEL28, YELLOW_6, SETFAM_1, FUNCT_1, XXREAL_0, LATTICES,
YELLOW_0, RELAT_1, RELAT_2, YELLOW_9, LATTICE3, YELLOW_2, YELLOW19,
MCART_1, CLASSES2, CLASSES1, METRIC_1, INT_2, RCOMP_1, FINSET_1, PROB_1,
CANTOR_1, RLVECT_3, ORDINAL1, PRELAMB, DIRAF, WAYBEL19, WAYBEL11,
WAYBEL_7, WAYBEL33, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1,
ORDERS_2, CARD_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0,
CLASSES1, CLASSES2, CANTOR_1, WAYBEL_0, YELLOW_1, YELLOW_6, YELLOW_2,
WAYBEL_3, WAYBEL_7, WAYBEL_9, WAYBEL11, COMPTS_1, YELLOW_9, WAYBEL19,
WAYBEL28, YELLOW19;
constructors CLASSES1, TOLER_1, CLASSES2, REALSET2, CANTOR_1, WAYBEL_1,
WAYBEL_3, WAYBEL_7, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL28, YELLOW19,
COMPTS_1, RELSET_1, TOPS_2, WAYBEL_2, XTUPLE_0, XFAMILY;
registrations SUBSET_1, RELAT_1, FINSET_1, CLASSES2, STRUCT_0, TOPS_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_7,
WAYBEL_9, YELLOW_9, WAYBEL19, YELLOW13, WAYBEL28, WAYBEL29, YELLOW19,
CARD_1, TEX_1, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, LATTICE3, YELLOW_6, WAYBEL_0, WAYBEL_7,
YELLOW_9, XBOOLE_0;
equalities SUBSET_1, YELLOW_6, WAYBEL_0, XBOOLE_0, STRUCT_0;
expansions TARSKI, SUBSET_1, PRE_TOPC, LATTICE3, WAYBEL_0, WAYBEL_7, XBOOLE_0;
theorems TARSKI, WAYBEL_7, WAYBEL_9, YELLOW_0, YELLOW_2, WAYBEL_0, PRE_TOPC,
LATTICE3, YELLOW_1, WAYBEL_8, ZFMISC_1, FUNCT_1, FUNCT_2, YELLOW_9,
WAYBEL28, YELLOW_6, SUBSET_1, WAYBEL23, WAYBEL21, CANTOR_1, WAYBEL11,
FRECHET2, CLASSES1, CLASSES2, YELLOW_4, FINSET_1, SETFAM_1, WAYBEL19,
WAYBEL32, YELLOW19, XBOOLE_0, XBOOLE_1, RELAT_1, STRUCT_0, XTUPLE_0;
schemes FUNCT_1, FUNCT_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
"\/"({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 Y2 = {inf B2 where B2 is Subset of L2: B2 in F2};
set Y1 = {inf B1 where B1 is Subset of L1: B1 in F1};
A3: Y2 c= Y1
proof
let x be object;
assume x in Y2;
then consider B2 being Subset of L2 such that
A4: x = inf B2 and
A5: B2 in F2;
F1 c= the carrier of BoolePoset X1;
then F1 c= bool X1 by WAYBEL_7:2;
then reconsider B1=B2 as Subset of L1 by A2,A5,XBOOLE_1:1;
inf B1 = inf B2 by A1,YELLOW_0:17,27;
hence thesis by A2,A4,A5;
end;
Y1 c= Y2
proof
let x be object;
assume x in Y1;
then consider B1 being Subset of L1 such that
A6: x = inf B1 and
A7: B1 in F1;
F2 c= the carrier of BoolePoset X2;
then F2 c= bool X2 by WAYBEL_7:2;
then reconsider B2=B1 as Subset of L2 by A2,A7,XBOOLE_1:1;
inf B1 = inf B2 by A1,YELLOW_0:17,27;
hence thesis by A2,A6,A7;
end;
then Y1 = Y2 by A3;
hence thesis by A1,YELLOW_0:17,26;
end;
definition
let L be non empty TopRelStr;
attr L is lim-inf means
: Def2:
the topology of L = xi L;
end;
registration
cluster lim-inf -> TopSpace-like for non empty TopRelStr;
coherence
proof
let L be non empty TopRelStr;
set T = ConvergenceSpace lim_inf-Convergence L;
assume L is lim-inf;
then
A1: the topology of L = xi L
.= the topology of T by WAYBEL28:def 4;
A2: 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;
reconsider b = a as Subset-Family of T by YELLOW_6:def 24;
assume a c= the topology of L;
then (union b) in the topology of T by A1,PRE_TOPC:def 1;
hence thesis by A1;
end;
the carrier of L = the carrier of T by YELLOW_6:def 24;
then
A3: the carrier of L in the topology of L by A1,PRE_TOPC:def 1;
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 A1,PRE_TOPC:def 1;
hence thesis by A3,A2;
end;
end;
registration
cluster trivial -> lim-inf for TopLattice;
coherence
proof
let L be TopLattice;
assume L is trivial;
then
the carrier of L is 1-element;
then reconsider L9 = L as 1-element TopLattice by STRUCT_0:def 19;
the carrier of ConvergenceSpace lim_inf-Convergence L = the carrier of
L9 by YELLOW_6:def 24;
then reconsider
S = ConvergenceSpace lim_inf-Convergence L as 1-element TopSpace
by STRUCT_0:def 19;
set x = the Point of L9;
reconsider y = x as Point of S by YELLOW_6:def 24;
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;
registration
cluster lim-inf continuous complete for TopLattice;
existence
proof
take the 1-element TopLattice;
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 11;
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 11;
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 and
A2: the mapping of N1 = the mapping of N2;
let j1 be Element of N1;
deffunc I2(Element of N2) = {N2.i where i is Element of N2: i >= $1};
deffunc I1(Element of N1) = {N1.i where i is Element of N1: i >= $1};
let j2 be Element of N2 such that
A3: j1 = j2;
thus I1(j1) c= I2(j2)
proof
let y be object;
assume y in I1(j1);
then consider i1 being Element of N1 such that
A4: y = N1.i1 and
A5: i1 >= j1;
reconsider i1 as Element of N1;
reconsider i2 = i1, j2 as Element of N2 by A1;
A6: N1.i1 = N2.i2 by A2;
i2 >= j2 by A1,A3,A5,YELLOW_0:1;
hence thesis by A4,A6;
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 and
A3: the mapping of N1 = the mapping of N2;
deffunc I2(Element of N2) = {N2.i where i is Element of N2: i >= $1};
deffunc I1(Element of N1) = {N1.i where i is Element of N1: i >= $1};
set U1 = the set of all "/\" (I1(j), L1) where j is Element of N1;
set U2 = the set of all "/\" (I2(j), L2) where j is Element of N2;
thus U1 c= U2
proof
let x be object;
assume x in U1;
then consider j1 being Element of N1 such that
A4: x = "/\"(I1(j1), L1);
reconsider j2 = j1 as Element of N2 by A2;
I1(j1) c= I2(j2) & I2(j2) c= I1(j1) by A2,A3,Lm1;
then
A5: I1(j1) = I2(j2);
reconsider j1 as Element of N1;
A6: I1(j1) c= the carrier of L1
proof
let x be object;
assume x in I1(j1);
then ex i being Element of N1 st x = N1.i & i >= j1;
hence thesis;
end;
[#]N1 is directed by WAYBEL_0:def 6;
then consider j0 being Element of N1 such that
j0 in the carrier of N1 and
A7: j1 <= j0 and
j1 <= j0;
N1.j0 in I1(j1) by A7;
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,A4,A5,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 I2(Element of N2) = {N2.i where i is Element of N2: i >= $1};
deffunc I1(Element of N1) = {N1.i where i is Element of N1: i >= $1};
set U1 = the set of all "/\" (I1(j), L1) where j is Element of N1;
set U2 = the set of all "/\" (I2(j), L2) where j is Element of N2;
A3: lim_inf N1 = "\/"(U1, L1) & lim_inf N2 = "\/"(U2, L2) by WAYBEL11:def 6;
U1 c= the carrier of L1
proof
let x be object;
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:7;
then
A4: ex_sup_of U1, L1 by WAYBEL_0:75;
U1 c= U2 & U2 c= U1 by A1,A2,Lm2;
then U1 = U2;
hence thesis by A1,A3,A4,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;
reconsider S2 as strict net of L2 by A4;
consider f being Function 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 9;
reconsider g = f as Function 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 thesis 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 18;
then consider N, x being object such that
A3: N in NetUniv L1 and
A4: x in the carrier of L1 and
A5: [N1,a] = [N,x] by A2,ZFMISC_1:def 2;
reconsider x as Element of L1 by A4;
A6: N = N1 by A5,XTUPLE_0:1;
then consider N2 being strict net of L2 such that
A7: N2 in NetUniv L2 and
A8: the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the
mapping of N2 by A1,A3,Th3;
ex N being strict net of L1 st N = N1 & the carrier of N in
the_universe_of the carrier of L1 by A3,A6,YELLOW_6:def 11;
then reconsider N1 as strict net of L1;
A9: now
let M being subnet of N2;
consider M1 being strict subnet of N1 such that
A10: the RelStr of M = the RelStr of M1 & the mapping of M = the
mapping of M1 by A1,A8,Th5;
thus x = lim_inf M1 by A2,A3,A5,A6,WAYBEL28:def 3
.= lim_inf M by A1,A10,Th4;
end;
take N2;
x = a by A5,XTUPLE_0:1;
hence thesis by A1,A7,A8,A9,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 and
A2: the mapping of N1 = the mapping of N2;
let X be set;
given i1 being Element of N1 such that
A3: 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 N1.j1 in X by A1,A3,YELLOW_0:1;
hence thesis by A2;
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 object;
A2: 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 24;
A3: 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 24;
assume x in the topology of ConvergenceSpace lim_inf-Convergence L1;
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 A3;
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
ex N1 being strict net of L1 st [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
;
hence N is_eventually_in V2 by A5,A6,Th7;
end;
hence thesis by A2,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 C2 = lim_inf-Convergence L2;
set C1 = lim_inf-Convergence L1;
set T1 = ConvergenceSpace C1;
set T2 = ConvergenceSpace C2;
the topology of T1 c= the topology of T2 & the topology of T2 c= the
topology of T1 by A1,Lm3;
then the carrier of T2 = the carrier of L2 & the topology of T1 = the
topology of T2 by YELLOW_6:def 24;
hence thesis by A1,YELLOW_6:def 24;
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;
assume
A1: the RelStr of L1 = the RelStr of L2;
xi L1 = the topology of ConvergenceSpace lim_inf-Convergence L1 & xi L2
= the topology of ConvergenceSpace lim_inf-Convergence L2 by WAYBEL28:def 4;
hence xi L1 c= xi L2 & xi L2 c= xi L1 by A1,Lm3;
end;
registration
let R be /\-complete non empty reflexive RelStr;
cluster -> /\-complete for 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 x >= v by A1,A3,YELLOW_0:2;
hence thesis by A1,YELLOW_0:1;
end;
end;
registration
let R be Semilattice;
cluster -> with_infima for 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 x9 = x, y9 = y as Element of R;
consider z9 being Element of R such that
A2: z9 <= x9 & z9 <= y9 and
A3: for v9 being Element of R st v9 <= x9 & v9 <= y9 holds v9 <= z9 by
LATTICE3:def 11;
reconsider z = z9 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 v9 = v as Element of R by A1;
assume v <= x & v <= y;
then v9 <= x9 & v9 <= y9 by A1,YELLOW_0:1;
then v9 <= z9 by A3;
hence v <= z by A1,YELLOW_0:1;
end;
end;
registration
let L be /\-complete up-complete Semilattice;
cluster strict lim-inf for 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 & 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,Th9;
end;
existence
proof
set T = TopRelStr(#the carrier of L, the InternalRel of L, xi L#);
A2: 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 A2,Th9;
end;
end;
registration
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 =
"\/"((the set of all inf (N|i) where i is Element of N), L)
proof
let L be complete LATTICE, N be net of L;
set X =the set of all
"/\"({N.i where i is Element of N:i >= j},L) where j is Element of N;
set Y =the set of all inf (N|i) where i is Element of N;
for x being object st x in X holds x in Y
proof
let x be object;
assume x in X;
then consider j being Element of N such that
A1: x = "/\"({N.i where i is Element of N : i >= j},L);
reconsider x as Element of L by A1;
set S = {N.i where i is Element of N : i >= j};
reconsider i=j as Element of N;
for b being object st b in rng the mapping of (N|i) holds b in S
proof
let b being object;
assume b in rng the mapping of (N|i);
then b in the set of all (N|i).k where k is Element of N|i by
WAYBEL11:19;
then consider k being Element of N|i such that
A2: b = (N|i).k;
the carrier of N|i c= the carrier of N by WAYBEL_9:13;
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
A3: ex y being Element of N st k = y & i <= y;
reconsider k as Element of N|i;
N.l = (N|i).k by WAYBEL_9:16;
hence thesis by A2,A3;
end;
then
A4: rng the mapping of (N|i) c= S;
A5: ex_inf_of S,L by YELLOW_0:17;
then
A6: S is_>=_than x by A1,YELLOW_0:def 10;
A7: rng the mapping of (N|i) is_>=_than x
by A6,A4;
for b being object st b in S holds b in rng the mapping of (N|i)
proof
let b being object;
assume b in S;
then consider k being Element of N such that
A8: b = N.k and
A9: 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 the set of all (N|i).m where m is Element of N|i by A8;
hence thesis by WAYBEL11:19;
end;
then S c= rng the mapping of (N|i);
then S = rng the mapping of (N|i) by A4;
then for a being Element of L st rng the mapping of (N|i) is_>=_than a
holds a <= x by A1,A5,YELLOW_0:def 10;
then consider i being Element of N such that
A10: 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 A7,YELLOW_0:17;
A11: 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;
x = "/\"(rng the mapping of (N|i),L) by A10,YELLOW_0:def 10;
hence thesis by A11;
end;
then
A12: lim_inf N = "\/"(X,L) & X c= Y by WAYBEL11:def 6;
for x being object st x in Y holds x in X
proof
let x being object;
assume x in Y;
then consider i being Element of N such that
A13: x = inf (N|i);
set S = {N.j where j is Element of N : j >= i};
for b being object st b in rng the mapping of (N|i) holds b in S
proof
let b being object;
assume b in rng the mapping of (N|i);
then b in the set of all (N|i).k where k is Element of N|i by
WAYBEL11:19;
then consider k being Element of N|i such that
A14: b = (N|i).k;
the carrier of N|i c= the carrier of N by WAYBEL_9:13;
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
A15: ex y being Element of N st k = y & i <= y;
reconsider k as Element of N|i;
N.l = (N|i).k by WAYBEL_9:16;
hence thesis by A14,A15;
end;
then
A16: rng the mapping of (N|i) c= S;
reconsider x as Element of L by A13;
A17: x = Inf the mapping of (N|i) by A13,WAYBEL_9:def 2
.= "/\"(rng the mapping of (N|i),L) by YELLOW_2:def 6;
for b being object st b in S holds b in rng the mapping of (N|i)
proof
let b being object;
assume b in S;
then consider k being Element of N such that
A18: b = N.k and
A19: k >= i;
reconsider l = k as Element of N;
l in { y where y is Element of N : i <= y} by A19;
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 the set of all (N|i).m where m is Element of N|i by A18;
hence thesis by WAYBEL11:19;
end;
then S c= rng the mapping of (N|i);
then rng the mapping of (N|i) = S by A16;
hence thesis by A17;
end;
then Y c= X;
hence thesis by A12,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;
for b being object st b in f holds b in rng the mapping of ((a_net F)|i)
proof
let b being object;
assume
A3: 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 A3;
then reconsider k = [b,f] as Element of (a_net F) by YELLOW19:def 4;
reconsider l = k as Element of (a_net F);
[b,f]`1 = b;
then
A4: b = (a_net F).k by YELLOW19:def 4;
k`2 c= i`2 by A2;
then i <= k by YELLOW19:def 4;
then l in { y where y is Element of (a_net F) : i <= y};
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 the set of all ((a_net F)|i).m where m is Element of (a_net F)|
i by A4;
hence thesis by WAYBEL11:19;
end;
then
A5: f c= rng the mapping of ((a_net F)|i);
for b being object st b in rng the mapping of ((a_net F)|i) holds b in f
proof
let b being object;
assume b in rng the mapping of ((a_net F)|i);
then
b in the set of all ((a_net F)|i).k where k is Element of (a_net F)|i
by WAYBEL11:19;
then consider k being Element of (a_net F)|i such that
A6: b = ((a_net F)|i).k;
A7: the carrier of (a_net F)|i c= the carrier of (a_net F) by WAYBEL_9:13;
then reconsider l = k as Element of a_net F;
k in the carrier of (a_net F) by A7;
then
A8: k in {[c, g] where c is Element of L, g is Element of F: c in g} by
YELLOW19:def 4;
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 ex y being Element of a_net F st k = y & i <= y;
then
A9: l`2 c= f by A2,YELLOW19:def 4;
consider c being Element of L, g being Element of F such that
A10: k = [c,g] and
A11: c in g by A8;
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 A6,YELLOW19:def 4;
hence thesis by A11,A9,A10;
end;
then
A12: rng the mapping of ((a_net F)|i) c= f;
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;
hence thesis by A12,A5,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 =the set of all inf ((a_net F)|i) where i is Element of a_net F;
set Y = {inf B where B is Subset of L: B in F};
for x being object st x in X holds x in Y
proof
let x be object;
assume x in X;
then consider i being Element of a_net F such that
A1: 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
A2: i = [a,f] and
a in f;
reconsider i as Element of a_net F;
reconsider f as Element of BoolePoset [#]L;
reconsider f as Subset of L by WAYBEL_7:2;
[a,f]`2 = f;
then inf f = inf ((a_net F)|i) by Th12,A2;
hence thesis by A1;
end;
then
A3: X c= Y;
for x being object st x in Y holds x in X
proof
let x be object;
assume x in Y;
then consider B being Subset of L such that
A4: x = inf B and
A5: B in F;
not Bottom (BoolePoset [#]L) in F by WAYBEL_7:4;
then B <> {} by A5,YELLOW_1:18;
then consider a being Element of L such that
A6: a in B by SUBSET_1:4;
reconsider B as Element of F by A5;
[a,B] in {[b,f] where b is Element of L, f is Element of F: b in f} by A6;
then reconsider i = [a,B] as Element of a_net F by YELLOW19:def 4;
[a,B]`2 = B;
then x = inf ((a_net F)|i) by A4,Th12;
hence thesis;
end;
then
A7: Y c= X;
lim_inf a_net F = "\/"(X,L) by Th11;
hence thesis by A3,A7,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 object;
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] and
a in f;
f is Subset of [#]L by WAYBEL_7:2;
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};
set UN = the_universe_of the carrier of L;
reconsider UN as universal set;
the_transitive-closure_of the carrier of L in UN by CLASSES1:2;
then
A1: the carrier of L in UN by CLASSES1:3,52;
then bool the carrier of L in UN by CLASSES2:59;
then
A2: [:the carrier of L, bool the carrier of L:] in UN by A1,CLASSES2:61;
S c= [:the carrier of L, bool the carrier of L:] by Lm4;
then S = the carrier of a_net F & S in UN by A2,CLASSES1:def 1,YELLOW19:def 4
;
hence thesis by YELLOW_6:def 11;
end;
theorem Th15:
for L being complete LATTICE, F being ultra Filter of BoolePoset
[#]L for p being greater_or_equal_to_id Function 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 Function of a_net F, a_net F;
set M = (a_net F)*p;
set rM = rng the mapping of M;
set C = the Element of F;
A1: inf M = Inf the mapping of M by WAYBEL_9:def 2
.= "/\"(rM,L) by YELLOW_2:def 6;
F c= the carrier of BoolePoset [#]L;
then F c= bool [#]L by WAYBEL_7:2;
then C in bool [#]L;
then
A2: C \ rM c= [#]L by XBOOLE_1:1;
then reconsider D=C \ rM, A=C /\ rM as Element of BoolePoset [#] L by
WAYBEL_7:2;
A3: the carrier of M = the carrier of a_net F by WAYBEL28:6;
then reconsider g = p as Function of M, a_net F;
A4: now
set d = the Element of D;
assume
A5: D in F;
not Bottom (BoolePoset [#]L) in F by WAYBEL_7:4;
then
A6: D <> {} by A5,YELLOW_1:18;
then
A7: d in D;
reconsider D as Element of F by A5;
reconsider d as Element of L by A2,A7;
[d,D] in {[a, f] where a is Element of L, f is Element of F: a in f} by A6;
then reconsider dD= [d,D] as Element of a_net F by YELLOW19:def 4;
reconsider dD9 = dD as Element of M by WAYBEL28:6;
A8: dom p = the carrier of a_net F by FUNCT_2:52;
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
A9: i = dD9;
take i;
for j being Element of M st j >= i holds g.j >= dD
proof
reconsider i9=i as Element of a_net F by WAYBEL28:6;
let j be Element of M;
reconsider j9=j as Element of a_net F by WAYBEL28:6;
A10: j9 <= g.j by WAYBEL28:def 1;
reconsider i9 as Element of a_net F;
reconsider j9 as Element of a_net F;
A11: the RelStr of M = the RelStr of a_net F by WAYBEL28:def 2;
assume j >= i;
then i9 <= j9 by A11,YELLOW_0:1;
hence thesis by A9,A10,YELLOW_0:def 2;
end;
hence thesis;
end;
then consider i being Element of M such that
A12: for j being Element of M st j >= i holds g.j >= dD;
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
A13: g.i >= dD by A12;
[d,D]`2 = D;
then
A14: (p.i)`2 c= D by A13,YELLOW19:def 4;
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
A15: g.i = [a, f] and
A16: a in f;
A17: (p.i)`1 in (p.i)`2 by A15,A16;
M.i = ((the mapping of a_net F)*p).i by WAYBEL28:def 2
.= (a_net F).G by A3,A8,FUNCT_1:13
.= (p.i)`1 by YELLOW19:def 4;
then not M.i in rM by A14,A17,XBOOLE_0:def 5;
hence contradiction by FUNCT_2:4;
end;
set Y = {inf B where B is Subset of L: B in F};
reconsider A9 = A as Subset of L;
A18: D"\/"A = D \/ A by YELLOW_1:17
.= C by XBOOLE_1:51;
F is prime by WAYBEL_7:22;
then A in F by A18,A4;
then inf A9 in Y;
then
A19: inf A9 <= lim_inf F by YELLOW_0:17,YELLOW_4:1;
A c= rM by XBOOLE_1:17;
then inf M <= inf A9 by A1,WAYBEL_7:1;
hence thesis by A19,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;
lim_inf F = lim_inf a_net F & for p being greater_or_equal_to_id
Function of a_net F, a_net F holds lim_inf F >= inf ((a_net F) * p) by Th13
,Th15;
hence thesis by WAYBEL28:14;
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 N9 being strict subnet of N st rng the mapping of N9
c= A & N9 is SubNetStr of N
proof
let L be non empty 1-sorted;
let N be net of L;
let A be set;
assume N is_often_in A;
then reconsider N9 = N"A as strict subnet of N by YELLOW_6:22;
take N9;
rng the mapping of N9 c= A
proof
let y be object;
assume y in rng the mapping of N9;
then consider x being object such that
A1: x in dom the mapping of N9 and
A2: y = (the mapping of N9).x by FUNCT_1:def 3;
A3: x in dom ((the mapping of N)|the carrier of N9) by A1,YELLOW_6:def 6;
then x in (dom the mapping of N) /\ the carrier of N9 by RELAT_1:61;
then x in the carrier of N9 by XBOOLE_0:def 4;
then
A4: x in (the mapping of N)"A by YELLOW_6:def 10;
y = ((the mapping of N)|the carrier of N9).x by A2,YELLOW_6:def 6;
then y = (the mapping of N).x by A3,FUNCT_1:47;
hence thesis by A4,FUNCT_1:def 7;
end;
hence thesis;
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;
xi L = the topology of ConvergenceSpace lim_inf-Convergence L by
WAYBEL28:def 4;
then
A1: 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 24;
set V = A`;
A2: the topology of L = xi L by Def2;
hereby
assume A is closed;
then A` in xi L by A2,PRE_TOPC:def 2;
then
A3: ex V being Subset of L st V = A` & 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 A1;
let F be ultra Filter of BoolePoset [#]L;
assume
A4: A in F;
( for M being subnet of a_net F holds lim_inf F = lim_inf M)& a_net F
in NetUniv L by Th14,Th16;
then
A5: [a_net F, lim_inf F] in lim_inf-Convergence L by WAYBEL28:def 3;
assume not lim_inf F in A;
then lim_inf F in A` by XBOOLE_0:def 5;
then a_net F is_eventually_in A` by A3,A5;
then consider i being Element of a_net F such that
A6: for j being Element of a_net F st i <= j holds (a_net F).j in A`;
A7: 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
A8: i = [a, f] and
a in f by A7;
reconsider A9 = A, f9 = f as Element of BoolePoset [#]L by A4;
consider B being Element of BoolePoset [#]L such that
A9: B in F and
A10: A9 >= B and
A11: f9 >= B by A4,WAYBEL_0:def 2;
set b = the Element of B;
not Bottom (BoolePoset [#]L) in F by WAYBEL_7:4;
then B is non empty by A9,YELLOW_1:18;
then
A12: b in B;
the carrier of BoolePoset [#]L = bool the carrier of L by WAYBEL_7:2;
then [b, B] in the carrier of a_net F by A7,A9,A12;
then reconsider j = [b, B] as Element of a_net F;
B c= f by A11,YELLOW_1:2;
then j`2 c= f;
then j`2 c= i`2 by A8;
then j >= i by YELLOW19:def 4;
then (a_net F).j in A` by A6;
then j`1 in A` by YELLOW19:def 4;
then
A13: b in A`;
B c= A by A10,YELLOW_1:2;
hence contradiction by A12,A13,XBOOLE_0:def 5;
end;
assume
A14: for F being ultra Filter of BoolePoset [#]L st A in F holds lim_inf
F in A;
now
let p be Element of L;
assume p in V;
then
A15: not p in V` by XBOOLE_0:def 5;
reconsider x = p as Element of L;
let N be net of L such that
A16: [N,p] in lim_inf-Convergence L;
assume not N is_eventually_in V;
then N is_often_in A by WAYBEL_0:10;
then consider N9 being strict subnet of N such that
A17: rng the mapping of N9 c= A and
A18: N9 is SubNetStr of N by Th17;
lim_inf-Convergence L c= [:NetUniv L, the carrier of L:] by YELLOW_6:def 18
;
then
A19: N in NetUniv L by A16,ZFMISC_1:87;
then
A20: ex N1 being strict net of L st N1 = N & the carrier of N1 in
the_universe_of the carrier of L by YELLOW_6:def 11;
set j0 = the Element of N9;
reconsider rj = rng the mapping of N9|j0, a = A as Element of BoolePoset
[#]L by WAYBEL_7:2;
set j2 = the Element of N9;
set G = the set of all rng the mapping of N9|j where j is Element of N9;
set g = rng the mapping of N9|j2;
A21: g in G;
for g being object st g in G holds g in the carrier of BoolePoset [#]L
proof
let g be object;
assume g in G;
then ex j3 being Element of N9 st g = rng the mapping of N9|j3;
then g in bool [#]L;
hence thesis by WAYBEL_7:2;
end;
then reconsider G as non empty Subset of BoolePoset [#]L by A21,
TARSKI:def 3;
A22: G c= fininfs G by WAYBEL_0:50;
now
let p be object;
assume p in rj;
then p in rng ((the mapping of N9)|the carrier of N9|j0) by
WAYBEL_9:def 7;
then consider q be object such that
A23: q in dom ((the mapping of N9)|the carrier of N9|j0) and
A24: p = ((the mapping of N9)|the carrier of N9|j0).q by FUNCT_1:def 3;
q in (dom the mapping of N9) /\ the carrier of N9|j0 by A23,RELAT_1:61;
then
A25: q in dom the mapping of N9 by XBOOLE_0:def 4;
p = (the mapping of N9).q by A23,A24,FUNCT_1:47;
hence p in rng the mapping of N9 by A25,FUNCT_1:3;
end;
then rj c= rng the mapping of N9;
then rj c= a by A17;
then rng the mapping of N9|j0 in G & rj <= a by YELLOW_1:2;
then
A26: a in uparrow fininfs G by A22,WAYBEL_0:def 16;
A27: x = lim_inf N9 by A16,A19,WAYBEL28:def 3;
then
A28: x = "\/"((the set of all inf (N9|j) where j is Element of N9), L) by Th11;
the carrier of N9 c= the carrier of N by A18,YELLOW_6:10;
then the carrier of N9 in the_universe_of the carrier of L by A20,
CLASSES1:def 1;
then
A29: N9 in NetUniv L by YELLOW_6:def 11;
A30: not {} in fininfs G
proof
assume {} in fininfs G;
then consider Y being finite Subset of G such that
A31: {} = "/\"(Y,BoolePoset [#]L) and
ex_inf_of Y, BoolePoset [#]L;
defpred P[object,object] means
ex j being Element of N9 st j = $2 & $1 = rng
the mapping of N9|j;
A32: "/\"({},BoolePoset [#]L) = Top BoolePoset [#]L by YELLOW_0:def 12
.= [#]L by YELLOW_1:19;
reconsider Y as finite Subset of BoolePoset [#]L by XBOOLE_1:1;
A33: for x being object st x in Y
ex y being object st y in the carrier of N9
& P[x,y]
proof
let x be object;
assume x in Y;
then x in G;
then
A34: ex j being Element of N9 st x = rng the mapping of N9|j;
assume for y being object st y in the carrier of N9 holds not P[x,y];
hence contradiction by A34;
end;
consider f being Function such that
A35: dom f = Y & rng f c= the carrier of N9 and
A36: for x being object st x in Y holds P[x,f.x] from FUNCT_1:sch 6(A33);
reconsider C = rng f as finite Subset of [#]N9 by A35,FINSET_1:8;
[#]N9 is directed by WAYBEL_0:def 6;
then consider j0 being Element of N9 such that
j0 in [#]N9 and
A37: j0 is_>=_than C by WAYBEL_0:1;
for y being set st y in Y holds rng the mapping of N9|j0 c= y
proof
let y be set such that
A38: y in Y;
consider j1 being Element of N9 such that
A39: j1 = f.y and
A40: y = rng the mapping of N9|j1 by A36,A38;
A41: f.y in rng f by A35,A38,FUNCT_1:3;
then reconsider f1=f.y as Element of N9 by A35;
A42: f1 <= j0 by A37,A41;
for p being object st p in rng the mapping of N9|j0 holds p in y
proof
let p be object;
assume p in rng the mapping of N9|j0;
then p in rng ((the mapping of N9)|the carrier of N9|j0) by
WAYBEL_9:def 7;
then consider q be object such that
A43: q in dom ((the mapping of N9)|the carrier of N9|j0) and
A44: p = ((the mapping of N9)|the carrier of N9|j0).q by FUNCT_1:def 3;
A45: q in (dom the mapping of N9) /\ the carrier of N9|j0 by A43,
RELAT_1:61;
then q in the carrier of N9|j0 by XBOOLE_0:def 4;
then q in { n9 where n9 is Element of N9 : j0 <=n9 } by WAYBEL_9:12;
then consider n9 being Element of N9 such that
A46: q = n9 and
A47: j0 <= n9;
f1 <= n9 by A42,A47,YELLOW_0:def 2;
then q in { m9 where m9 is Element of N9 : j1 <=m9 } by A39,A46;
then
A48: q in the carrier of N9|j1 by WAYBEL_9:12;
q in dom the mapping of N9 by A45,XBOOLE_0:def 4;
then q in (dom the mapping of N9) /\ the carrier of N9|j1 by A48,
XBOOLE_0:def 4;
then
A49: q in dom ((the mapping of N9)|the carrier of N9|j1) by RELAT_1:61;
p = (the mapping of N9).q by A43,A44,FUNCT_1:47;
then p = ((the mapping of N9)|the carrier of N9|j1).q by A49,
FUNCT_1:47;
then p in rng((the mapping of N9)|the carrier of N9|j1) by A49,
FUNCT_1:3;
hence thesis by A40,WAYBEL_9:def 7;
end;
hence thesis;
end;
then rng the mapping of N9|j0 c= meet Y by A31,A32,SETFAM_1:5;
then rng the mapping of N9|j0 c= {} by A31,A32,YELLOW_1:20;
hence contradiction;
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;
assume (Bottom BoolePoset [#]L) >= y;
then {} = Bottom BoolePoset [#]L & y c= Bottom BoolePoset [#]L by
YELLOW_1:2,18;
hence thesis by A30;
end;
then not Bottom BoolePoset [#]L in uparrow fininfs G by WAYBEL_0:def 16;
then uparrow fininfs G is proper;
then consider F being Filter of BoolePoset [#]L such that
A50: uparrow fininfs G c= F and
A51: F is ultra by WAYBEL_7:26;
A52: fininfs G c= uparrow fininfs G by WAYBEL_0:16;
A53: the set of all inf (N9|j) where j is Element of N9 c= {inf f
where f is Subset of L: f in F}
proof
let x be object;
assume x in the set of all inf (N9|j) where j is Element of N9;
then consider j3 being Element of N9 such that
A54: x = inf (N9|j3);
reconsider f1 = rng the mapping of (N9|j3) as Subset of L;
fininfs G c= F by A50,A52;
then
A55: f1 in G & G c= F by A22;
x = Inf the mapping of (N9|j3) by A54,WAYBEL_9:def 2
.= "/\"(rng the mapping of (N9|j3),L) by YELLOW_2:def 6;
hence thesis by A55;
end;
now
let M be subnet of N9;
M is subnet of N by YELLOW_6:15;
hence x = lim_inf M by A16,A19,WAYBEL28:def 3;
end;
then
A56: for M being subnet of N9 st M in NetUniv L holds x = lim_inf M;
{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
A57: y = inf f0 and
A58: f0 in F;
defpred P[Element of N9,Element of N9] means $1 <= $2 & N9.$2 in f0;
A59: now
let j be Element of N9;
not Bottom (BoolePoset [#]L) in F by A51,WAYBEL_7:4;
then
A60: not {} in F by YELLOW_1:18;
G c= uparrow fininfs G by A22,A52;
then
A61: G c= F by A50;
rng the mapping of N9|j in G;
then f0 /\ rng the mapping of N9|j in F by A58,A61,WAYBEL_7:9;
then consider nj being Element of L such that
A62: nj in f0 /\ rng the mapping of N9|j by A60,SUBSET_1:4;
nj in rng the mapping of N9|j by A62,XBOOLE_0:def 4;
then consider pj9 being object such that
A63: pj9 in dom the mapping of N9|j and
A64: nj=(the mapping of N9|j).pj9 by FUNCT_1:def 3;
pj9 in the carrier of (N9|j) by A63;
then pj9 in { y9 where y9 is Element of N9 : j <= y9 } by WAYBEL_9:12;
then consider pj being Element of N9 such that
A65: pj = pj9 and
A66: j <= pj;
reconsider pj9 as Element of (N9|j) by A63;
take pj;
N9.pj = (N9|j).pj9 by A65,WAYBEL_9:16
.=(the mapping of N9|j).pj9;
hence P[j,pj] by A62,A64,A66,XBOOLE_0:def 4;
end;
consider p being Function of N9, N9 such that
A67: for j being Element of N9 holds P[j,p.j] from FUNCT_2:sch 3(A59);
for b being object st b in rng the mapping of (N9*p) holds b in f0
proof
let b be object;
assume b in rng the mapping of (N9*p);
then b in the set of all (N9*p).k where k is Element of N9*p
by WAYBEL11:19;
then consider k being Element of N9*p such that
A68: b = (N9*p).k;
reconsider l = k as Element of N9 by WAYBEL28:6;
the carrier of N9*p = the carrier of N9 by WAYBEL28:6;
then k in the carrier of N9;
then
A69: k in dom p by FUNCT_2:52;
(N9*p).k = ((the mapping of N9)*p).k by WAYBEL28:def 2
.= N9.(p.l) by A69,FUNCT_1:13;
hence thesis by A67,A68;
end;
then rng the mapping of (N9*p) c= f0;
then
A70: "/\"(f0,L) <= "/\"(rng the mapping of (N9*p),L) by WAYBEL_7:1;
A71: for M being subnet of N9 st M in NetUniv L holds x >= inf M by A29,A56,
WAYBEL28:3;
p is greater_or_equal_to_id by A67,WAYBEL28:def 1;
then
A72: inf (N9*p) <= x by A29,A27,A71,WAYBEL28:13;
inf (N9*p) = Inf the mapping of N9*p by WAYBEL_9:def 2
.= "/\"(rng the mapping of (N9*p),L) by YELLOW_2:def 6;
hence thesis by A57,A72,A70,YELLOW_0:def 2;
end;
then
A73: lim_inf F <= x by YELLOW_0:32;
ex_sup_of {inf f where f is Subset of L: f in F}, L & ex_sup_of (the set of
all inf
(N9|j) where j is Element of N9), L by YELLOW_0:17;
then x <= lim_inf F by A28,A53,YELLOW_0:34;
then x = lim_inf F by A73,YELLOW_0:def 3;
hence contradiction by A14,A50,A51,A26,A15;
end;
then A` in xi L by A1;
then A` is open by A2;
hence thesis;
end;
theorem Th19:
for L being non empty reflexive RelStr holds sigma L c= xi L
by WAYBEL28:28;
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 and
A2: the carrier of T1 in the topology of T2;
let x be object;
FinMeetCl B is Basis of T1 by YELLOW_9:23;
then
A3: the topology of T1 = UniCl FinMeetCl B by YELLOW_9:22;
assume x in the topology of T1;
then consider Y being Subset-Family of T1 such that
A4: Y c= FinMeetCl B and
A5: x = union Y by A3,CANTOR_1:def 1;
A6: Y c= the topology of T2
proof
let y be object;
assume y in Y;
then consider Z being Subset-Family of T1 such that
A7: Z c= B and
A8: Z is finite and
A9: y = Intersect Z by A4,CANTOR_1:def 3;
Z c= the topology of T2 by A1,A7;
then reconsider Z9 = Z as Subset-Family of T2 by XBOOLE_1:1;
y = the carrier of T1 or Z9 c= the topology of T2 & y = meet Z9 &
meet Z9 = Intersect Z9 by A1,A7,A9,SETFAM_1:def 9;
then y = the carrier of T1 or y in FinMeetCl the topology of T2 by A8,
CANTOR_1:def 3;
hence thesis by A2,CANTOR_1:5;
end;
then reconsider Y as Subset-Family of T2 by XBOOLE_1:1;
union Y in UniCl the topology of T2 by A6,CANTOR_1:def 1;
hence thesis by A5,CANTOR_1:6;
end;
theorem Th21:
for L being complete LATTICE holds omega L c= xi L
proof
let L be complete LATTICE;
set S = the lower correct TopAugmentation of L;
set X = the lim-inf TopAugmentation of L;
reconsider B = the set of all (uparrow x)` where x is Element of S as
prebasis of S by WAYBEL19:def 1;
A1: the RelStr of S = the RelStr of L & the RelStr of X = the RelStr of L by
YELLOW_9:def 4;
A2: B c= the topology of X
proof
let b be object;
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;
set A = uparrow y;
X is SubRelStr of X by YELLOW_6:6;
then S is SubRelStr of X by A1,WAYBEL21:12;
then
A4: uparrow x c= uparrow y by WAYBEL23:14;
A5: 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:22;
hence lim_inf F in A by A5,WAYBEL_0:18;
end;
then
A6: A is closed by Th18;
S is SubRelStr of S by YELLOW_6:6;
then X is SubRelStr of S by A1,WAYBEL21:12;
then uparrow y c= uparrow x by WAYBEL23:14;
then uparrow y = uparrow x by A4;
hence thesis by A1,A3,A6,PRE_TOPC:def 2;
end;
the carrier of S in the topology of X by A1,PRE_TOPC:def 1;
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) 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:14;
then the topology of R c= UniCl FinMeetCl the topology of T by A5,A6,
CANTOR_1:9;
hence thesis 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;
let A be Subset of T1;
A1: the carrier of T1 = the carrier of T2 by YELLOW_9:def 5;
reconsider B = A as Subset of T2 by YELLOW_9:def 5;
reconsider C = [#]T2 \ B as Subset of T2;
A2: the topology of T1 c= the topology of T2 by YELLOW_9:def 5;
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 A2;
hence thesis by PRE_TOPC:def 2;
end;
assume [#]T1 \ A in the topology of T1;
then C is open by A2,A1;
hence thesis by PRE_TOPC:def 3;
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;
set T = the Lawson correct TopAugmentation of L;
set S = the Scott TopAugmentation of L;
set LL = the lower correct TopAugmentation of L;
set LI = the lim-inf TopAugmentation of L;
A1: the RelStr of LI = the RelStr of L by YELLOW_9:def 4;
A2: xi L = the topology of LI by Th10;
omega L = the topology of LL by WAYBEL19:def 2;
then the RelStr of LL = the RelStr of L & the topology of LL c= xi L by Th21,
YELLOW_9:def 4;
then
A3: LI is TopExtension of LL by A2,A1,YELLOW_9:def 5;
sigma L = the topology of S by YELLOW_9:51;
then the RelStr of S = the RelStr of L & the topology of S c= xi L by Th19,
YELLOW_9:def 4;
then T is Refinement of S,LL & LI is TopExtension of S by A2,A1,WAYBEL19:29
,YELLOW_9:def 5;
then lambda L = the topology of T & LI is TopExtension of T by A3,Th22,
WAYBEL19:def 4;
hence thesis by A2,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;
lambda L = the topology of S & xi L = the topology of T by Th10,
WAYBEL19:def 4;
then
A1: the topology of S c= the topology of T by Th24;
the RelStr of T = the RelStr of L & the RelStr of S = the RelStr of L by
YELLOW_9:def 4;
hence thesis by A1,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;
let A be Subset of L;
assume that
A1: A is open and
A2: x in A and
A3: not A in F;
F is prime by WAYBEL_7:22;
then
A4: ([#]L)\A in F by A3,WAYBEL_7:21;
then A` <> {} by YELLOW19:1;
then x in A` by A1,A4,Th18;
hence contradiction by A2,XBOOLE_0:def 5;
end;
::$N Compactness of Lim-inf Topology
theorem :: 3.6. PROPOSITION (A), p. 169(?)
for L being complete lim-inf TopLattice holds L is compact T_1
proof
let L be complete lim-inf TopLattice;
set T = the Lawson correct TopAugmentation of L;
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:31;
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
A1: L is TopExtension of T by Th25;
{z} is closed;
then {y} is closed by A1,Th23;
hence Cl {x} = {x} by PRE_TOPC:22;
end;
hence thesis by FRECHET2:43;
end;