:: WAYBEL33 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem defines lim_inf WAYBEL33:def 1 :
theorem :: WAYBEL33:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def2 defines lim-inf WAYBEL33:def 2 :
theorem Th2: :: WAYBEL33:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: WAYBEL33:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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)
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
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: WAYBEL33:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: WAYBEL33:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: WAYBEL33:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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))
theorem :: WAYBEL33:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: WAYBEL33:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: WAYBEL33:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def3 defines Xi WAYBEL33:def 3 :
theorem Th11: :: WAYBEL33:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: WAYBEL33:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: WAYBEL33:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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):]
theorem Th14: :: WAYBEL33:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: WAYBEL33:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: WAYBEL33:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: WAYBEL33:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: WAYBEL33:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: WAYBEL33:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: WAYBEL33:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: WAYBEL33:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: WAYBEL33:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th23: :: WAYBEL33:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: WAYBEL33:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: WAYBEL33:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th26: :: WAYBEL33:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: WAYBEL33:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 