:: by Grzegorz Bancerek and Noboru Endou

::

:: Received July 29, 2001

:: Copyright (c) 2001-2016 Association of Mizar Users

definition

let L be non empty Poset;

let X be non empty Subset of L;

let F be Filter of (BoolePoset X);

coherence

"\/" ( { (inf B) where B is Subset of L : B in F } ,L) is Element of L;

;

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

coherence

"\/" ( { (inf B) where B is Subset of L : B in F } ,L) is Element of L;

;

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

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

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;

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

for L being non empty TopRelStr holds

( L is lim-inf iff the topology of L = xi L );

registration

coherence

for b_{1} being non empty TopRelStr st b_{1} is lim-inf holds

b_{1} is TopSpace-like

end;
for b

b

proof end;

registration

for b_{1} being TopLattice st b_{1} is trivial holds

b_{1} is lim-inf
end;

cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima -> lim-inf for TopRelStr ;

coherence for b

b

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is lim-inf & b_{1} is continuous & b_{1} is complete )
end;

cluster non empty TopSpace-like reflexive transitive antisymmetric continuous with_suprema with_infima complete lim-inf for TopRelStr ;

existence ex b

( b

proof 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 )

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 )

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

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 )

proof end;

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

H_{2}(j1) c= H_{1}(j2)

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

H

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

H_{2}(j1) c= H_{1}(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

H_{2}(j1) c= H_{1}(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

H_{2}(j1) c= H_{1}(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

H_{2}(j1) c= H_{1}(j2)

let j1 be Element of N1; :: thesis: for j2 being Element of N2 st j1 = j2 holds

H_{2}(j1) c= H_{1}(j2)

deffunc H_{1}( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;

deffunc H_{2}( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;

let j2 be Element of N2; :: thesis: ( j1 = j2 implies H_{2}(j1) c= H_{1}(j2) )

assume A3: j1 = j2 ; :: thesis: H_{2}(j1) c= H_{1}(j2)

thus H_{2}(j1) c= H_{1}(j2)
:: thesis: verum

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

H

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

H

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

H

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

H

let j1 be Element of N1; :: thesis: for j2 being Element of N2 st j1 = j2 holds

H

deffunc H

deffunc H

let j2 be Element of N2; :: thesis: ( j1 = j2 implies H

assume A3: j1 = j2 ; :: thesis: H

thus H

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H_{2}(j1) or y in H_{1}(j2) )

assume y in H_{2}(j1)
; :: thesis: y in H_{1}(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 H_{1}(j2)
by A4, A6; :: thesis: verum

end;
assume y in H

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 H

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

{ ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum }

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

{ ("/\" (H

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

{ ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(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

{ ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(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

{ ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(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 { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(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: { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum }

deffunc H_{1}( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;

deffunc H_{2}( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;

set U1 = { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } ;

set U2 = { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum } ;

thus { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum }
:: thesis: verum

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

{ ("/\" (H

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

{ ("/\" (H

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

{ ("/\" (H

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 { ("/\" (H

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: { ("/\" (H

deffunc H

deffunc H

set U1 = { ("/\" (H

set U2 = { ("/\" (H

thus { ("/\" (H

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum } or x in { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum } )

assume x in { ("/\" (H_{2}(j),L1)) where j is Element of N1 : verum }
; :: thesis: x in { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum }

then consider j1 being Element of N1 such that

A4: x = "/\" (H_{2}(j1),L1)
;

reconsider j2 = j1 as Element of N2 by A2;

( H_{2}(j1) c= H_{1}(j2) & H_{1}(j2) c= H_{2}(j1) )
by A2, A3, Lm1;

then A5: H_{2}(j1) = H_{1}(j2)
;

reconsider j1 = j1 as Element of N1 ;

A6: H_{2}(j1) c= the carrier of L1

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 H_{2}(j1)
by A7;

then reconsider S = H_{2}(j1) as non empty Subset of L1 by A6;

ex_inf_of S,L1 by WAYBEL_0:76;

then x = "/\" (H_{1}(j2),L2)
by A1, A4, A5, YELLOW_0:27;

hence x in { ("/\" (H_{1}(j),L2)) where j is Element of N2 : verum }
; :: thesis: verum

end;
assume x in { ("/\" (H

then consider j1 being Element of N1 such that

A4: x = "/\" (H

reconsider j2 = j1 as Element of N2 by A2;

( H

then A5: H

reconsider j1 = j1 as Element of N1 ;

A6: H

proof

[#] N1 is directed
by WAYBEL_0:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{2}(j1) or x in the carrier of L1 )

assume x in H_{2}(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;
assume x in H

then ex i being Element of N1 st

( x = N1 . i & i >= j1 ) ;

hence x in the carrier of L1 ; :: thesis: verum

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 H

then reconsider S = H

ex_inf_of S,L1 by WAYBEL_0:76;

then x = "/\" (H

hence x in { ("/\" (H

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

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 )

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 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 & 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 )

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 & 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 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 #) & 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

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 #) & 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)

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

xi L1 = xi L2

proof end;

registration

let R be non empty reflexive /\-complete RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is /\-complete

end;
coherence

for b

proof end;

registration

let R be Semilattice;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is with_infima

end;
coherence

for b

proof end;

registration

let L be up-complete /\-complete Semilattice;

ex b_{1} being TopAugmentation of L st

( b_{1} is strict & b_{1} is lim-inf )

end;
cluster non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict lim-inf for TopAugmentation of L;

existence ex b

( b

proof 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

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;

uniqueness

for b_{1}, b_{2} being strict TopAugmentation of L st b_{1} is lim-inf & b_{2} is lim-inf holds

b_{1} = b_{2}

ex b_{1} being strict TopAugmentation of L st b_{1} is lim-inf

end;
uniqueness

for b

b

proof end;

existence ex b

proof end;

:: deftheorem Def3 defines Xi WAYBEL33:def 3 :

for L being up-complete /\-complete Semilattice

for b_{2} being strict TopAugmentation of L holds

( b_{2} = Xi L iff b_{2} is lim-inf );

for L being up-complete /\-complete Semilattice

for b

( b

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)

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)

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)

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

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)

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

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 )

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 )

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

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

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

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

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

for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L

proof end;

:: Compactness of Lim-inf Topology