:: Compactness of Lim-inf Topology
:: by Grzegorz Bancerek and Noboru Endou
::
:: Received July 29, 2001
:: Copyright (c) 2001-2012 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
proofend;

definition
let L be non empty TopRelStr ;
attrL 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 for TopRelStr ;
coherence
 for b1 being non empty TopRelStr st b1 is lim-inf holds
b1 is TopSpace-like
proofend;
end;

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

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric continuous with_suprema with_infima complete lim-inf for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is lim-inf & b1 is continuous & b1 is complete )
proofend;
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 over L1 ex N2 being strict NetStr over 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 )
proofend;

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 over 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 )
proofend;

Lm1: now__::_thesis:_for_L1,_L2_being_non_empty_RelStr_
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 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 toTARSKI: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__::_thesis:_for_L1,_L2_being_/\-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_
{__("/\"_(H2(j),L1))_where_j_is_Element_of_N1_:_verum__}__c=__{__("/\"_(H1(j),L2))_where_j_is_Element_of_N2_:_verum__}_
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 toTARSKI: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 toTARSKI: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 #) &amp; the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2
proofend;

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 #) &amp; 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 #) &amp; the mapping of S1 = the mapping of S2 )
proofend;

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 over 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 &amp; RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) &amp; the mapping of N1 = the mapping of N2 )
proofend;

theorem Th7: :: WAYBEL33:7
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 RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) &amp; 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
proofend;

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))
proofend;

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)
proofend;

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
proofend;

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

registration
let R be Semilattice;
cluster  ->  with_infima for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is with_infima
proofend;
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 for TopAugmentation of L;
existence
 ex b1 being TopAugmentation of L st
( b1 is strict &amp; b1 is lim-inf )
proofend;
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
proofend;

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 &amp; b2 is lim-inf holds
b1 = b2
proofend;
existence
 ex b1 being strict TopAugmentation of L st b1 is lim-inf
proofend;
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)
proofend;

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)
proofend;

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)
proofend;

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):]
proofend;

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

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)
proofend;

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
proofend;

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 &amp; N9 is SubNetStr of N )
proofend;

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 )
proofend;

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

theorem Th20: :: WAYBEL33:20
for T1, T2 being non empty TopSpace
for B being prebasis of T1 st B c= the topology of T2 &amp; the carrier of T1 in the topology of T2 holds
the topology of T1 c= the topology of T2
proofend;

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

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

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 ) &amp; ( A is closed implies A is closed Subset of T2 ) )
proofend;

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

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
proofend;

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
proofend;

:: [WP: ] Compactness_of_Lim-inf_Topology
theorem :: WAYBEL33:27
for L being complete lim-inf TopLattice holds
( L is compact &amp; L is T_1 )
proofend;