:: Compactness of Lim-inf Topology
:: by Grzegorz Bancerek and Noboru Endou
::
:: Received July 29, 2001
:: Copyright (c) 2001-2011 Association of Mizar Users


begin

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 :: WAYBEL33:def 1
 "\/" ( { (inf B) where B is Subset of L : B in F } ,L);
correctness
coherence
"\/" ( { (inf B) where B is Subset of L : B in F } ,L) is Element of L;
;
end;

:: deftheorem defines lim_inf WAYBEL33:def 1 :
for L being non empty Poset
for X being non empty Subset of L
for F being Filter of (BoolePoset X) holds lim_inf F = "\/" ( { (inf B) where B is Subset of L : B in F } ,L);

theorem :: WAYBEL33:1
for L1, L2 being complete LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
proof end;

definition
let L be non empty TopRelStr ;
attr L is lim-inf means :Def2: :: WAYBEL33:def 2
 the topology of L = xi L;
end;

:: deftheorem Def2 defines lim-inf WAYBEL33:def 2 :
for L being non empty TopRelStr holds
( L is lim-inf iff the topology of L = xi L );

registration
cluster non empty lim-inf -> non empty TopSpace-like TopRelStr ;
coherence
for b1 being non empty TopRelStr st b1 is lim-inf holds
b1 is TopSpace-like
proof end;
end;

registration
cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima -> lim-inf TopRelStr ;
coherence
for b1 being TopLattice st b1 is trivial holds
b1 is lim-inf
proof end;
end;

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric continuous with_suprema with_infima complete lim-inf TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is lim-inf & b1 is continuous & b1 is complete )
proof end;
end;

theorem Th2: :: WAYBEL33:2
for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr of L1 ex N2 being strict NetStr of L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
proof end;

theorem Th3: :: WAYBEL33:3
for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr of L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
proof end;

Lm1: now
let L1, L2 be non empty RelStr ; :: thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
let N1 be net of L1; :: thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
let N2 be net of L2; :: thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2) )
assume that
A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A2: the mapping of N1 = the mapping of N2 ; :: thesis: for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
let j1 be Element of N1; :: thesis: for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
let j2 be Element of N2; :: thesis: ( j1 = j2 implies H2(j1) c= H1(j2) )
assume A3: j1 = j2 ; :: thesis: H2(j1) c= H1(j2)
thus H2(j1) c= H1(j2) :: thesis: verum
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in H2(j1) or y in H1(j2) )
assume y in H2(j1) ; :: thesis: y in H1(j2)
then consider i1 being Element of N1 such that
A4: y = N1 . i1 and
A5: i1 >= j1 ;
reconsider i1 = i1 as Element of N1 ;
reconsider i2 = i1, j2 = j2 as Element of N2 by A1;
A6: N1 . i1 = N2 . i2 by A2;
i2 >= j2 by A1, A3, A5, YELLOW_0:1;
hence y in H1(j2) by A4, A6; :: thesis: verum
end;
end;

Lm2: now
let L1, L2 be /\-complete Semilattice; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
let N1 be net of L1; :: thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
let N2 be net of L2; :: thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } )
assume that
A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A3: the mapping of N1 = the mapping of N2 ; :: thesis: { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
set U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ;
set U2 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ;
thus { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } :: thesis: verum
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } or x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } )
assume x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; :: thesis: x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
then consider j1 being Element of N1 such that
A4: x = "/\" (H2(j1),L1) ;
reconsider j2 = j1 as Element of N2 by A2;
( H2(j1) c= H1(j2) & H1(j2) c= H2(j1) ) by A2, A3, Lm1;
then A5: H2(j1) = H1(j2) by XBOOLE_0:def 10;
reconsider j1 = j1 as Element of N1 ;
A6: H2(j1) c= the carrier of L1
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H2(j1) or x in the carrier of L1 )
assume x in H2(j1) ; :: thesis: x in the carrier of L1
then ex i being Element of N1 st
( x = N1 . i & i >= j1 ) ;
hence x in the carrier of L1 ; :: thesis: verum
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 by WAYBEL_0:def 1;
N1 . j0 in H2(j1) by A7;
then reconsider S = H2(j1) as non empty Subset of L1 by A6;
ex_inf_of S,L1 by WAYBEL_0:76;
then x = "/\" (H1(j2),L2) by A1, A4, A5, YELLOW_0:27;
hence x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ; :: thesis: verum
end;
end;

theorem Th4: :: WAYBEL33:4
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2
proof end;

theorem Th5: :: WAYBEL33:5
for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
proof end;

theorem Th6: :: WAYBEL33:6
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being NetStr of L1
for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
proof end;

theorem Th7: :: WAYBEL33:7
for L1, L2 being non empty 1-sorted
for N1 being non empty NetStr of L1
for N2 being non empty NetStr of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X
proof end;

Lm3: for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2))
proof end;

theorem :: WAYBEL33:8
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2)
proof end;

theorem Th9: :: WAYBEL33:9
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
xi L1 = xi L2
proof end;

registration
let R be non empty reflexive /\-complete RelStr ;
cluster -> /\-complete TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is /\-complete
proof end;
end;

registration
let R be Semilattice;
cluster -> with_infima TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is with_infima
proof end;
end;

registration
let L be up-complete /\-complete Semilattice;
cluster non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict lim-inf TopAugmentation of L;
existence
ex b1 being TopAugmentation of L st
( b1 is strict & b1 is lim-inf )
proof end;
end;

theorem Th10: :: WAYBEL33:10
for L being up-complete /\-complete Semilattice
for X being lim-inf TopAugmentation of L holds xi L = the topology of X
proof end;

definition
let L be up-complete /\-complete Semilattice;
func Xi L -> strict TopAugmentation of L means :Def3: :: WAYBEL33:def 3
it is lim-inf ;
uniqueness
for b1, b2 being strict TopAugmentation of L st b1 is lim-inf & b2 is lim-inf holds
b1 = b2
proof end;
existence
ex b1 being strict TopAugmentation of L st b1 is lim-inf
proof end;
end;

:: deftheorem Def3 defines Xi WAYBEL33:def 3 :
for L being up-complete /\-complete Semilattice
for b2 being strict TopAugmentation of L holds
( b2 = Xi L iff b2 is lim-inf );

registration
let L be up-complete /\-complete Semilattice;
cluster Xi L -> strict lim-inf ;
coherence
Xi L is lim-inf by Def3;
end;

theorem Th11: :: WAYBEL33:11
for L being complete LATTICE
for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)
proof end;

theorem Th12: :: WAYBEL33:12
for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L))
for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
proof end;

theorem Th13: :: WAYBEL33:13
for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F)
proof end;

Lm4: for L being LATTICE
for 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 end;

theorem Th14: :: WAYBEL33:14
for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L
proof end;

theorem Th15: :: WAYBEL33:15
for L being complete LATTICE
for 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 end;

theorem Th16: :: WAYBEL33:16
for L being complete LATTICE
for F being ultra Filter of (BoolePoset ([#] L))
for M being subnet of a_net F holds lim_inf F = lim_inf M
proof end;

theorem Th17: :: WAYBEL33:17
for L being non empty 1-sorted
for N being net of L
for A being set st N is_often_in A holds
ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
proof end;

theorem Th18: :: WAYBEL33:18
for L being complete lim-inf TopLattice
for 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 end;

theorem Th19: :: WAYBEL33:19
for L being non empty reflexive RelStr holds sigma L c= xi L
proof end;

theorem Th20: :: WAYBEL33:20
for T1, T2 being non empty TopSpace
for 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 end;

theorem Th21: :: WAYBEL33:21
for L being complete LATTICE holds omega L c= xi L
proof end;

theorem Th22: :: WAYBEL33:22
for T1, T2 being TopSpace
for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds
for R being Refinement of T1,T2 holds T is TopExtension of R
proof end;

theorem Th23: :: WAYBEL33:23
for T1 being TopSpace
for 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 end;

theorem Th24: :: WAYBEL33:24
for L being complete LATTICE holds lambda L c= xi L
proof end;

theorem Th25: :: WAYBEL33:25
for L being complete LATTICE
for T being lim-inf TopAugmentation of L
for S being correct Lawson TopAugmentation of L holds T is TopExtension of S
proof end;

theorem Th26: :: WAYBEL33:26
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 end;

theorem :: WAYBEL33:27
for L being complete lim-inf TopLattice holds
( L is compact & L is T_1 )
proof end;