:: WAYBEL33 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> lim-inf TopRelStr ;
coherence
for b1 being TopLattice st b1 is trivial holds
b1 is lim-inf
proof end;
end;

registration
cluster continuous 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
H1(j1) c= H2(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
H1(j1) c= H2(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
H1(j1) c= H2(j2) )
assume A1: ( 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 ) ; :: thesis: for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H1(j1) c= H2(j2)
deffunc H1( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
deffunc H2( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
let j1 be Element of N1; :: thesis: for j2 being Element of N2 st j1 = j2 holds
H1(j1) c= H2(j2)
let j2 be Element of N2; :: thesis: ( j1 = j2 implies H1(j1) c= H2(j2) )
assume A2: j1 = j2 ; :: thesis: H1(j1) c= H2(j2)
thus H1(j1) c= H2(j2) :: thesis: verum
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in H1(j1) or y in H2(j2) )
assume y in H1(j1) ; :: thesis: y in H2(j2)
then consider i1 being Element of N1 such that
A3: ( y = N1 . i1 & i1 >= j1 ) ;
reconsider i1 = i1, j1 = j1 as Element of N1 ;
reconsider i2 = i1, j2 = j2 as Element of N2 by A1;
A4: i2 >= j2 by A1, A2, A3, YELLOW_0:1;
N1 . i1 = the mapping of N1 . i1
.= N2 . i2 by A1 ;
hence y in H2(j2) by A3, A4; :: 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
{ ("/\" H1(j),L1) where j is Element of N1 : verum } c= { ("/\" H2(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
{ ("/\" H1(j),L1) where j is Element of N1 : verum } c= { ("/\" H2(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
{ ("/\" H1(j),L1) where j is Element of N1 : verum } c= { ("/\" H2(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 { ("/\" H1(j),L1) where j is Element of N1 : verum } c= { ("/\" H2(j),L2) where j is Element of N2 : verum } )
assume A2: ( 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 ) ; :: thesis: { ("/\" H1(j),L1) where j is Element of N1 : verum } c= { ("/\" H2(j),L2) where j is Element of N2 : verum }
deffunc H1( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
deffunc H2( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
set U1 = { ("/\" H1(j),L1) where j is Element of N1 : verum } ;
set U2 = { ("/\" H2(j),L2) where j is Element of N2 : verum } ;
thus { ("/\" H1(j),L1) where j is Element of N1 : verum } c= { ("/\" H2(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 { ("/\" H1(j),L1) where j is Element of N1 : verum } or x in { ("/\" H2(j),L2) where j is Element of N2 : verum } )
assume x in { ("/\" H1(j),L1) where j is Element of N1 : verum } ; :: thesis: x in { ("/\" H2(j),L2) where j is Element of N2 : verum }
then consider j1 being Element of N1 such that
A3: x = "/\" H1(j1),L1 ;
reconsider j2 = j1 as Element of N2 by A2;
A4: H1(j1) = H2(j2)
proof
thus ( H1(j1) c= H2(j2) & H2(j2) c= H1(j1) ) by A2, Lm1; :: according to XBOOLE_0:def 10 :: thesis: verum
end;
reconsider j1 = j1 as Element of N1 ;
( [#] N1 = the carrier of N1 & [#] N1 is directed ) by WAYBEL_0:def 6;
then consider j0 being Element of N1 such that
j0 in the carrier of N1 and
A5: ( j1 <= j0 & j1 <= j0 ) by WAYBEL_0:def 1;
A6: N1 . j0 in H1(j1) by A5;
H1(j1) c= the carrier of L1
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(j1) or x in the carrier of L1 )
assume x in H1(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;
then reconsider S = H1(j1) as non empty Subset of L1 by A6;
ex_inf_of S,L1 by WAYBEL_0:76;
then x = "/\" H2(j2),L2 by A1, A3, A4, YELLOW_0:27;
hence x in { ("/\" H2(j),L2) where j is Element of N2 : verum } ; :: thesis: verum
end;
end;

theorem Th4: :: WAYBEL33:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 TopSpace-like /\-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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> TopSpace-like /\-complete with_infima strict lim-inf ;
coherence
Xi L is lim-inf by Def3;
end;

theorem Th11: :: WAYBEL33:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 N' being strict subnet of N st
( rng the mapping of N' c= A & N' is SubNetStr of N )
proof end;

theorem Th18: :: WAYBEL33:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive RelStr holds sigma L c= xi L
proof end;

theorem Th20: :: WAYBEL33:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE holds omega L c= xi L
proof end;

theorem Th22: :: WAYBEL33:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE holds lambda L c= xi L
proof end;

theorem Th25: :: WAYBEL33:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete lim-inf TopLattice holds
( L is compact & L is being_T1 )
proof end;