:: WAYBEL_9 semantic presentation
begin
registration
let L be non empty RelStr ;
cluster id L -> monotone ;
coherence
id L is monotone by YELLOW_2:11;
end;
definition
let S, T be non empty RelStr ;
let f be Function of S,T;
redefine attr f is antitone means :Def1: :: WAYBEL_9:def 1
for x, y being Element of S st x <= y holds
f . x >= f . y;
compatibility
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y )
proof
thus ( f is antitone implies for x, y being Element of S st x <= y holds
f . x >= f . y ) by WAYBEL_0:def_5; ::_thesis: ( ( for x, y being Element of S st x <= y holds
f . x >= f . y ) implies f is antitone )
assume for x, y being Element of S st x <= y holds
f . x >= f . y ; ::_thesis: f is antitone
hence for x, y being Element of S st x <= y holds
for a, b being Element of T st a = f . x & b = f . y holds
a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: verum
end;
end;
:: deftheorem Def1 defines antitone WAYBEL_9:def_1_:_
for S, T being non empty RelStr
for f being Function of S,T holds
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y );
theorem Th1: :: WAYBEL_9:1
for S, T being RelStr
for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
proof
let S, T be RelStr ; ::_thesis: for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
let K, L be non empty RelStr ; ::_thesis: for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
let f be Function of S,T; ::_thesis: for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
let g be Function of K,L; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone implies g is monotone )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) and
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) and
A3: f = g and
A4: f is monotone ; ::_thesis: g is monotone
reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;
let x, y be Element of K; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y )
assume A5: x <= y ; ::_thesis: g . x <= g . y
reconsider x1 = x, y1 = y as Element of S1 by A1;
reconsider f1 = f as Function of S1,T1 ;
x1 <= y1 by A1, A5, YELLOW_0:1;
then f1 . x1 <= f1 . y1 by A4, WAYBEL_1:def_2;
hence g . x <= g . y by A2, A3, YELLOW_0:1; ::_thesis: verum
end;
theorem Th2: :: WAYBEL_9:2
for S, T being RelStr
for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
proof
let S, T be RelStr ; ::_thesis: for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
let K, L be non empty RelStr ; ::_thesis: for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
let f be Function of S,T; ::_thesis: for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
let g be Function of K,L; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone implies g is antitone )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) and
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) and
A3: f = g and
A4: f is antitone ; ::_thesis: g is antitone
reconsider S1 = S, T1 = T as non empty RelStr by A1, A2;
let x, y be Element of K; :: according to WAYBEL_9:def_1 ::_thesis: ( x <= y implies g . x >= g . y )
assume A5: x <= y ; ::_thesis: g . x >= g . y
reconsider x1 = x, y1 = y as Element of S1 by A1;
reconsider f1 = f as Function of S1,T1 ;
x1 <= y1 by A1, A5, YELLOW_0:1;
then f1 . x1 >= f1 . y1 by A4, Def1;
hence g . x >= g . y by A2, A3, YELLOW_0:1; ::_thesis: verum
end;
theorem :: WAYBEL_9:3
for A, B being 1-sorted
for F being Subset-Family of A
for G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds
G is Cover of B ;
Lm1: for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }
let x be Element of L; ::_thesis: uparrow x = { z where z is Element of L : z "/\" x = x }
thus uparrow x c= { z where z is Element of L : z "/\" x = x } :: according to XBOOLE_0:def_10 ::_thesis: { z where z is Element of L : z "/\" x = x } c= uparrow x
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow x or q in { z where z is Element of L : z "/\" x = x } )
assume A1: q in uparrow x ; ::_thesis: q in { z where z is Element of L : z "/\" x = x }
then reconsider q1 = q as Element of L ;
x <= q1 by A1, WAYBEL_0:18;
then q1 "/\" x = x by YELLOW_0:25;
hence q in { z where z is Element of L : z "/\" x = x } ; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { z where z is Element of L : z "/\" x = x } or q in uparrow x )
assume q in { z where z is Element of L : z "/\" x = x } ; ::_thesis: q in uparrow x
then consider z being Element of L such that
A2: q = z and
A3: z "/\" x = x ;
x <= z by A3, YELLOW_0:25;
hence q in uparrow x by A2, WAYBEL_0:18; ::_thesis: verum
end;
theorem Th4: :: WAYBEL_9:4
for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds uparrow x = {x} "\/" ([#] L)
proof
let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for x being Element of L holds uparrow x = {x} "\/" ([#] L)
let x be Element of L; ::_thesis: uparrow x = {x} "\/" ([#] L)
A1: {x} "\/" ([#] L) = { (x "\/" s) where s is Element of L : s in [#] L } by YELLOW_4:15;
thus uparrow x c= {x} "\/" ([#] L) :: according to XBOOLE_0:def_10 ::_thesis: {x} "\/" ([#] L) c= uparrow x
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow x or q in {x} "\/" ([#] L) )
assume A2: q in uparrow x ; ::_thesis: q in {x} "\/" ([#] L)
then reconsider q1 = q as Element of L ;
x <= q1 by A2, WAYBEL_0:18;
then x "\/" q1 = q1 by YELLOW_0:24;
hence q in {x} "\/" ([#] L) by A1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "\/" ([#] L) or q in uparrow x )
assume q in {x} "\/" ([#] L) ; ::_thesis: q in uparrow x
then consider z being Element of L such that
A3: q = x "\/" z and
z in [#] L by A1;
x <= x "\/" z by YELLOW_0:22;
hence q in uparrow x by A3, WAYBEL_0:18; ::_thesis: verum
end;
Lm2: for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }
proof
let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }
let x be Element of L; ::_thesis: downarrow x = { z where z is Element of L : z "\/" x = x }
thus downarrow x c= { z where z is Element of L : z "\/" x = x } :: according to XBOOLE_0:def_10 ::_thesis: { z where z is Element of L : z "\/" x = x } c= downarrow x
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow x or q in { z where z is Element of L : z "\/" x = x } )
assume A1: q in downarrow x ; ::_thesis: q in { z where z is Element of L : z "\/" x = x }
then reconsider q1 = q as Element of L ;
x >= q1 by A1, WAYBEL_0:17;
then q1 "\/" x = x by YELLOW_0:24;
hence q in { z where z is Element of L : z "\/" x = x } ; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { z where z is Element of L : z "\/" x = x } or q in downarrow x )
assume q in { z where z is Element of L : z "\/" x = x } ; ::_thesis: q in downarrow x
then consider z being Element of L such that
A2: q = z and
A3: z "\/" x = x ;
x >= z by A3, YELLOW_0:24;
hence q in downarrow x by A2, WAYBEL_0:17; ::_thesis: verum
end;
theorem Th5: :: WAYBEL_9:5
for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds downarrow x = {x} "/\" ([#] L)
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L holds downarrow x = {x} "/\" ([#] L)
let x be Element of L; ::_thesis: downarrow x = {x} "/\" ([#] L)
A1: {x} "/\" ([#] L) = { (x "/\" s) where s is Element of L : s in [#] L } by YELLOW_4:42;
thus downarrow x c= {x} "/\" ([#] L) :: according to XBOOLE_0:def_10 ::_thesis: {x} "/\" ([#] L) c= downarrow x
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow x or q in {x} "/\" ([#] L) )
assume A2: q in downarrow x ; ::_thesis: q in {x} "/\" ([#] L)
then reconsider q1 = q as Element of L ;
x >= q1 by A2, WAYBEL_0:17;
then x "/\" q1 = q1 by YELLOW_0:25;
hence q in {x} "/\" ([#] L) by A1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" ([#] L) or q in downarrow x )
assume q in {x} "/\" ([#] L) ; ::_thesis: q in downarrow x
then consider z being Element of L such that
A3: q = x "/\" z and
z in [#] L by A1;
x "/\" z <= x by YELLOW_0:23;
hence q in downarrow x by A3, WAYBEL_0:17; ::_thesis: verum
end;
theorem :: WAYBEL_9:6
for L being reflexive antisymmetric with_infima RelStr
for y being Element of L holds (y "/\") .: (uparrow y) = {y}
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for y being Element of L holds (y "/\") .: (uparrow y) = {y}
let y be Element of L; ::_thesis: (y "/\") .: (uparrow y) = {y}
thus (y "/\") .: (uparrow y) c= {y} :: according to XBOOLE_0:def_10 ::_thesis: {y} c= (y "/\") .: (uparrow y)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (y "/\") .: (uparrow y) or q in {y} )
assume q in (y "/\") .: (uparrow y) ; ::_thesis: q in {y}
then consider a being set such that
a in dom (y "/\") and
A1: a in uparrow y and
A2: q = (y "/\") . a by FUNCT_1:def_6;
reconsider a = a as Element of L by A1;
A3: y <= a by A1, WAYBEL_0:18;
q = y "/\" a by A2, WAYBEL_1:def_18
.= y by A3, YELLOW_0:25 ;
hence q in {y} by TARSKI:def_1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {y} or q in (y "/\") .: (uparrow y) )
assume q in {y} ; ::_thesis: q in (y "/\") .: (uparrow y)
then A4: q = y by TARSKI:def_1;
y <= y ;
then A5: ( dom (y "/\") = the carrier of L & y in uparrow y ) by FUNCT_2:def_1, WAYBEL_0:18;
y = y "/\" y by YELLOW_0:25
.= (y "/\") . y by WAYBEL_1:def_18 ;
hence q in (y "/\") .: (uparrow y) by A4, A5, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th7: :: WAYBEL_9:7
for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds (x "/\") " {x} = uparrow x
proof
let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for x being Element of L holds (x "/\") " {x} = uparrow x
let x be Element of L; ::_thesis: (x "/\") " {x} = uparrow x
thus (x "/\") " {x} c= uparrow x :: according to XBOOLE_0:def_10 ::_thesis: uparrow x c= (x "/\") " {x}
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (x "/\") " {x} or q in uparrow x )
assume A1: q in (x "/\") " {x} ; ::_thesis: q in uparrow x
then reconsider q1 = q as Element of L ;
A2: (x "/\") . q1 in {x} by A1, FUNCT_1:def_7;
x "/\" q1 = (x "/\") . q1 by WAYBEL_1:def_18
.= x by A2, TARSKI:def_1 ;
then x <= q1 by YELLOW_0:25;
hence q in uparrow x by WAYBEL_0:18; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow x or q in (x "/\") " {x} )
assume A3: q in uparrow x ; ::_thesis: q in (x "/\") " {x}
then reconsider q1 = q as Element of L ;
A4: x <= q1 by A3, WAYBEL_0:18;
(x "/\") . q1 = x "/\" q1 by WAYBEL_1:def_18
.= x by A4, YELLOW_0:25 ;
then ( dom (x "/\") = the carrier of L & (x "/\") . q1 in {x} ) by FUNCT_2:def_1, TARSKI:def_1;
hence q in (x "/\") " {x} by FUNCT_1:def_7; ::_thesis: verum
end;
theorem Th8: :: WAYBEL_9:8
for T being non empty 1-sorted
for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N
proof
let T be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over T holds N is_eventually_in rng the mapping of N
let N be non empty NetStr over T; ::_thesis: N is_eventually_in rng the mapping of N
set i = the Element of N;
take the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in rng the mapping of N )
let j be Element of N; ::_thesis: ( not the Element of N <= j or N . j in rng the mapping of N )
assume the Element of N <= j ; ::_thesis: N . j in rng the mapping of N
thus N . j in rng the mapping of N by FUNCT_2:4; ::_thesis: verum
end;
Lm3: for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L
let D be non empty directed Subset of L; ::_thesis: for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L
let n be Function of D, the carrier of L; ::_thesis: NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L
set N = NetStr(# D,( the InternalRel of L |_2 D),n #);
the InternalRel of NetStr(# D,( the InternalRel of L |_2 D),n #) c= the InternalRel of L by XBOOLE_1:17;
then reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as SubRelStr of L by YELLOW_0:def_13;
reconsider N = N as full SubRelStr of L by YELLOW_0:def_14;
N is directed
proof
let x, y be Element of N; :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] N or not y in [#] N or ex b1 being Element of the carrier of N st
( b1 in [#] N & x <= b1 & y <= b1 ) )
assume that
x in [#] N and
y in [#] N ; ::_thesis: ex b1 being Element of the carrier of N st
( b1 in [#] N & x <= b1 & y <= b1 )
reconsider x1 = x, y1 = y as Element of D ;
consider z1 being Element of L such that
A1: z1 in D and
A2: ( x1 <= z1 & y1 <= z1 ) by WAYBEL_0:def_1;
reconsider z = z1 as Element of N by A1;
take z ; ::_thesis: ( z in [#] N & x <= z & y <= z )
thus z in [#] N ; ::_thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A2, YELLOW_0:60; ::_thesis: verum
end;
then reconsider N = N as prenet of L ;
N is transitive ;
hence NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L ; ::_thesis: verum
end;
registration
let L be non empty reflexive RelStr ;
let D be non empty directed Subset of L;
let n be Function of D, the carrier of L;
cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> directed ;
coherence
NetStr(# D,( the InternalRel of L |_2 D),n #) is directed by WAYBEL_2:19;
end;
registration
let L be non empty reflexive transitive RelStr ;
let D be non empty directed Subset of L;
let n be Function of D, the carrier of L;
cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> transitive ;
coherence
NetStr(# D,( the InternalRel of L |_2 D),n #) is transitive by Lm3;
end;
theorem Th9: :: WAYBEL_9:9
for L being non empty reflexive transitive RelStr st ( for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
L is satisfying_MC
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: ( ( for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is satisfying_MC )
assume A1: for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: L is satisfying_MC
let x be Element of L; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of K10( the carrier of L) holds x "/\" ("\/" (b1,L)) = "\/" (({x} "/\" b1),L)
let D be non empty directed Subset of L; ::_thesis: x "/\" ("\/" (D,L)) = "\/" (({x} "/\" D),L)
reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7;
set N = NetStr(# D,( the InternalRel of L |_2 D),n #);
A2: ( NetStr(# D,( the InternalRel of L |_2 D),n #) is eventually-directed & Sup = sup NetStr(# D,( the InternalRel of L |_2 D),n #) ) by WAYBEL_2:20;
D c= D ;
then A3: D = n .: D by FUNCT_1:92
.= rng (netmap (NetStr(# D,( the InternalRel of L |_2 D),n #),L)) by RELSET_1:22 ;
hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def_5
.= sup ({x} "/\" D) by A1, A3, A2 ;
::_thesis: verum
end;
theorem Th10: :: WAYBEL_9:10
for L being non empty RelStr
for a being Element of L
for N being net of L holds a "/\" N is net of L
proof
let L be non empty RelStr ; ::_thesis: for a being Element of L
for N being net of L holds a "/\" N is net of L
let a be Element of L; ::_thesis: for N being net of L holds a "/\" N is net of L
let N be net of L; ::_thesis: a "/\" N is net of L
set aN = a "/\" N;
a "/\" N is transitive
proof
let x, y, z be Element of (a "/\" N); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume A1: ( x <= y & y <= z ) ; ::_thesis: x <= z
reconsider x1 = x, y1 = y, z1 = z as Element of N by WAYBEL_2:22;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (a "/\" N), the InternalRel of (a "/\" N) #) by WAYBEL_2:def_3;
then ( x1 <= y1 & y1 <= z1 ) by A1, YELLOW_0:1;
then x1 <= z1 by YELLOW_0:def_2;
hence x <= z by A2, YELLOW_0:1; ::_thesis: verum
end;
hence a "/\" N is net of L ; ::_thesis: verum
end;
registration
let L be non empty RelStr ;
let x be Element of L;
let N be net of L;
clusterx "/\" N -> transitive ;
coherence
x "/\" N is transitive by Th10;
end;
registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty reflexive NetStr over L;
clusterx "/\" N -> reflexive ;
coherence
x "/\" N is reflexive
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3;
then the InternalRel of (x "/\" N) is_reflexive_in the carrier of (x "/\" N) by ORDERS_2:def_2;
hence x "/\" N is reflexive by ORDERS_2:def_2; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty antisymmetric NetStr over L;
clusterx "/\" N -> antisymmetric ;
coherence
x "/\" N is antisymmetric
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3;
then the InternalRel of (x "/\" N) is_antisymmetric_in the carrier of (x "/\" N) by ORDERS_2:def_4;
hence x "/\" N is antisymmetric by ORDERS_2:def_4; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty transitive NetStr over L;
clusterx "/\" N -> transitive ;
coherence
x "/\" N is transitive
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3;
then the InternalRel of (x "/\" N) is_transitive_in the carrier of (x "/\" N) by ORDERS_2:def_3;
hence x "/\" N is transitive by ORDERS_2:def_3; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
let J be set ;
let f be Function of J, the carrier of L;
cluster FinSups f -> transitive ;
coherence
FinSups f is transitive
proof
let x, y, z be Element of (FinSups f); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
A3: ( ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) ) by WAYBEL_2:def_2, YELLOW_1:def_1;
then reconsider x1 = x, y1 = y, z1 = z as Element of (InclPoset (Fin J)) ;
y1 <= z1 by A2, A3, YELLOW_0:1;
then A4: y1 c= z1 by YELLOW_1:3;
x1 <= y1 by A1, A3, YELLOW_0:1;
then x1 c= y1 by YELLOW_1:3;
then x1 c= z1 by A4, XBOOLE_1:1;
then x1 <= z1 by YELLOW_1:3;
hence x <= z by A3, YELLOW_0:1; ::_thesis: verum
end;
end;
begin
definition
let L be non empty RelStr ;
let N be NetStr over L;
func inf N -> Element of L equals :: WAYBEL_9:def 2
Inf ;
coherence
Inf is Element of L ;
end;
:: deftheorem defines inf WAYBEL_9:def_2_:_
for L being non empty RelStr
for N being NetStr over L holds inf N = Inf ;
definition
let L be RelStr ;
let N be NetStr over L;
pred ex_sup_of N means :Def3: :: WAYBEL_9:def 3
ex_sup_of rng the mapping of N,L;
pred ex_inf_of N means :Def4: :: WAYBEL_9:def 4
ex_inf_of rng the mapping of N,L;
end;
:: deftheorem Def3 defines ex_sup_of WAYBEL_9:def_3_:_
for L being RelStr
for N being NetStr over L holds
( ex_sup_of N iff ex_sup_of rng the mapping of N,L );
:: deftheorem Def4 defines ex_inf_of WAYBEL_9:def_4_:_
for L being RelStr
for N being NetStr over L holds
( ex_inf_of N iff ex_inf_of rng the mapping of N,L );
definition
let L be RelStr ;
funcL +id -> strict NetStr over L means :Def5: :: WAYBEL_9:def 5
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of it = id L );
existence
ex b1 being strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b1 = id L )
proof
take NetStr(# the carrier of L, the InternalRel of L,(id L) #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of L, the InternalRel of L,(id L) #), the InternalRel of NetStr(# the carrier of L, the InternalRel of L,(id L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of NetStr(# the carrier of L, the InternalRel of L,(id L) #) = id L )
thus ( RelStr(# the carrier of NetStr(# the carrier of L, the InternalRel of L,(id L) #), the InternalRel of NetStr(# the carrier of L, the InternalRel of L,(id L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of NetStr(# the carrier of L, the InternalRel of L,(id L) #) = id L ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b1 = id L & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b2 = id L holds
b1 = b2 ;
end;
:: deftheorem Def5 defines +id WAYBEL_9:def_5_:_
for L being RelStr
for b2 being strict NetStr over L holds
( b2 = L +id iff ( RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b2 = id L ) );
registration
let L be non empty RelStr ;
clusterL +id -> non empty strict ;
coherence
not L +id is empty
proof
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5;
hence not L +id is empty ; ::_thesis: verum
end;
end;
registration
let L be reflexive RelStr ;
clusterL +id -> reflexive strict ;
coherence
L +id is reflexive
proof
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5;
then the InternalRel of (L +id) is_reflexive_in the carrier of (L +id) by ORDERS_2:def_2;
hence L +id is reflexive by ORDERS_2:def_2; ::_thesis: verum
end;
end;
registration
let L be antisymmetric RelStr ;
clusterL +id -> antisymmetric strict ;
coherence
L +id is antisymmetric
proof
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5;
then the InternalRel of (L +id) is_antisymmetric_in the carrier of (L +id) by ORDERS_2:def_4;
hence L +id is antisymmetric by ORDERS_2:def_4; ::_thesis: verum
end;
end;
registration
let L be transitive RelStr ;
clusterL +id -> transitive strict ;
coherence
L +id is transitive
proof
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5;
then the InternalRel of (L +id) is_transitive_in the carrier of (L +id) by ORDERS_2:def_3;
hence L +id is transitive by ORDERS_2:def_3; ::_thesis: verum
end;
end;
registration
let L be with_suprema RelStr ;
clusterL +id -> strict directed ;
coherence
L +id is directed
proof
A1: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) by Def5;
then [#] L = [#] (L +id) ;
hence [#] (L +id) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
registration
let L be directed RelStr ;
clusterL +id -> strict directed ;
coherence
L +id is directed
proof
( [#] L is directed & RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) ) by Def5, WAYBEL_0:def_6;
hence [#] (L +id) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
clusterL +id -> strict monotone eventually-directed ;
coherence
( L +id is monotone & L +id is eventually-directed )
proof
set N = L +id ;
( netmap ((L +id),L) = id L & RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by Def5;
then netmap ((L +id),L) is monotone by Th1;
hence L +id is monotone by WAYBEL_0:def_9; ::_thesis: L +id is eventually-directed
for i being Element of (L +id) ex j being Element of (L +id) st
for k being Element of (L +id) st j <= k holds
(L +id) . i <= (L +id) . k
proof
let i be Element of (L +id); ::_thesis: ex j being Element of (L +id) st
for k being Element of (L +id) st j <= k holds
(L +id) . i <= (L +id) . k
take j = i; ::_thesis: for k being Element of (L +id) st j <= k holds
(L +id) . i <= (L +id) . k
let k be Element of (L +id); ::_thesis: ( j <= k implies (L +id) . i <= (L +id) . k )
assume A1: j <= k ; ::_thesis: (L +id) . i <= (L +id) . k
A2: RelStr(# the carrier of (L +id), the InternalRel of (L +id) #) = RelStr(# the carrier of L, the InternalRel of L #) by Def5;
the mapping of (L +id) = id L by Def5;
then ( the mapping of (L +id) . i = i & the mapping of (L +id) . k = k ) by A2, FUNCT_1:18;
hence (L +id) . i <= (L +id) . k by A1, A2, YELLOW_0:1; ::_thesis: verum
end;
hence L +id is eventually-directed by WAYBEL_0:11; ::_thesis: verum
end;
end;
definition
let L be RelStr ;
funcL opp+id -> strict NetStr over L means :Def6: :: WAYBEL_9:def 6
( the carrier of it = the carrier of L & the InternalRel of it = the InternalRel of L ~ & the mapping of it = id L );
existence
ex b1 being strict NetStr over L st
( the carrier of b1 = the carrier of L & the InternalRel of b1 = the InternalRel of L ~ & the mapping of b1 = id L )
proof
take NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) ; ::_thesis: ( the carrier of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the carrier of L & the InternalRel of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the InternalRel of L ~ & the mapping of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = id L )
thus ( the carrier of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the carrier of L & the InternalRel of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = the InternalRel of L ~ & the mapping of NetStr(# the carrier of L,( the InternalRel of L ~),(id L) #) = id L ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict NetStr over L st the carrier of b1 = the carrier of L & the InternalRel of b1 = the InternalRel of L ~ & the mapping of b1 = id L & the carrier of b2 = the carrier of L & the InternalRel of b2 = the InternalRel of L ~ & the mapping of b2 = id L holds
b1 = b2 ;
end;
:: deftheorem Def6 defines opp+id WAYBEL_9:def_6_:_
for L being RelStr
for b2 being strict NetStr over L holds
( b2 = L opp+id iff ( the carrier of b2 = the carrier of L & the InternalRel of b2 = the InternalRel of L ~ & the mapping of b2 = id L ) );
theorem Th11: :: WAYBEL_9:11
for L being RelStr holds RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #)
proof
let L be RelStr ; ::_thesis: RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #)
the InternalRel of (L ~) = the InternalRel of (L opp+id) by Def6;
hence RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) by Def6; ::_thesis: verum
end;
registration
let L be non empty RelStr ;
clusterL opp+id -> non empty strict ;
coherence
not L opp+id is empty
proof
RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) by Th11;
hence not L opp+id is empty ; ::_thesis: verum
end;
end;
registration
let L be reflexive RelStr ;
clusterL opp+id -> reflexive strict ;
coherence
L opp+id is reflexive
proof
the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def_2;
then A1: the InternalRel of L ~ is_reflexive_in the carrier of L by ORDERS_1:79;
the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6;
hence the InternalRel of (L opp+id) is_reflexive_in the carrier of (L opp+id) by A1, Def6; :: according to ORDERS_2:def_2 ::_thesis: verum
end;
end;
registration
let L be antisymmetric RelStr ;
clusterL opp+id -> antisymmetric strict ;
coherence
L opp+id is antisymmetric
proof
the InternalRel of L is_antisymmetric_in the carrier of L by ORDERS_2:def_4;
then A1: the InternalRel of L ~ is_antisymmetric_in the carrier of L by ORDERS_1:81;
the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6;
then the InternalRel of (L opp+id) is_antisymmetric_in the carrier of (L opp+id) by A1, Def6;
hence L opp+id is antisymmetric by ORDERS_2:def_4; ::_thesis: verum
end;
end;
registration
let L be transitive RelStr ;
clusterL opp+id -> transitive strict ;
coherence
L opp+id is transitive
proof
the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def_3;
then A1: the InternalRel of L ~ is_transitive_in the carrier of L by ORDERS_1:80;
the InternalRel of (L opp+id) = the InternalRel of L ~ by Def6;
then the InternalRel of (L opp+id) is_transitive_in the carrier of (L opp+id) by A1, Def6;
hence L opp+id is transitive by ORDERS_2:def_3; ::_thesis: verum
end;
end;
registration
let L be with_infima RelStr ;
clusterL opp+id -> strict directed ;
coherence
L opp+id is directed
proof
reconsider A = L ~ as with_suprema RelStr by YELLOW_7:16;
( RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) & [#] A = [#] (L opp+id) ) by Def6, Th11;
hence [#] (L opp+id) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
clusterL opp+id -> strict antitone eventually-filtered ;
coherence
( L opp+id is antitone & L opp+id is eventually-filtered )
proof
set N = L opp+id ;
thus L opp+id is antitone ::_thesis: L opp+id is eventually-filtered
proof
reconsider f = id L as Function of (L ~),L ;
reconsider g = f as Function of L,(L ~) ;
g is antitone by YELLOW_7:40;
then A1: ( RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of L, the InternalRel of L #) & f is antitone ) by YELLOW_7:41;
( netmap ((L opp+id),L) = id L & RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #) = RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) ) by Def6, Th11;
hence netmap ((L opp+id),L) is antitone by A1, Th2; :: according to WAYBEL_0:def_10 ::_thesis: verum
end;
for i being Element of (L opp+id) ex j being Element of (L opp+id) st
for k being Element of (L opp+id) st j <= k holds
(L opp+id) . i >= (L opp+id) . k
proof
let i be Element of (L opp+id); ::_thesis: ex j being Element of (L opp+id) st
for k being Element of (L opp+id) st j <= k holds
(L opp+id) . i >= (L opp+id) . k
take j = i; ::_thesis: for k being Element of (L opp+id) st j <= k holds
(L opp+id) . i >= (L opp+id) . k
A2: ( the mapping of (L opp+id) = id L & the InternalRel of (L opp+id) = the InternalRel of L ~ ) by Def6;
let k be Element of (L opp+id); ::_thesis: ( j <= k implies (L opp+id) . i >= (L opp+id) . k )
assume j <= k ; ::_thesis: (L opp+id) . i >= (L opp+id) . k
then [i,k] in the InternalRel of (L opp+id) by ORDERS_2:def_5;
then A3: [k,i] in the InternalRel of (L opp+id) ~ by RELAT_1:def_7;
reconsider i1 = i, k1 = k as Element of L by Def6;
( (id L) . i1 = i1 & (id L) . k1 = k1 ) by FUNCT_1:18;
hence (L opp+id) . i >= (L opp+id) . k by A2, A3, ORDERS_2:def_5; ::_thesis: verum
end;
hence L opp+id is eventually-filtered by WAYBEL_0:12; ::_thesis: verum
end;
end;
definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let i be Element of N;
funcN | i -> strict NetStr over L means :Def7: :: WAYBEL_9:def 7
( ( for x being set holds
( x in the carrier of it iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of it = the InternalRel of N |_2 the carrier of it & the mapping of it = the mapping of N | the carrier of it );
existence
ex b1 being strict NetStr over L st
( ( for x being set holds
( x in the carrier of b1 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 & the mapping of b1 = the mapping of N | the carrier of b1 )
proof
defpred S1[ set ] means ex y being Element of N st
( y = $1 & i <= y );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of N & S1[x] ) ) from XBOOLE_0:sch_1();
X c= the carrier of N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of N )
assume x in X ; ::_thesis: x in the carrier of N
hence x in the carrier of N by A1; ::_thesis: verum
end;
then reconsider f = the mapping of N | X as Function of X, the carrier of L by FUNCT_2:32;
set IT = NetStr(# X,( the InternalRel of N |_2 X),f #);
take NetStr(# X,( the InternalRel of N |_2 X),f #) ; ::_thesis: ( ( for x being set holds
( x in the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) )
thus for x being set holds
( x in the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) iff ex y being Element of N st
( y = x & i <= y ) ) by A1; ::_thesis: ( the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) )
thus ( the InternalRel of NetStr(# X,( the InternalRel of N |_2 X),f #) = the InternalRel of N |_2 the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) & the mapping of NetStr(# X,( the InternalRel of N |_2 X),f #) = the mapping of N | the carrier of NetStr(# X,( the InternalRel of N |_2 X),f #) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict NetStr over L st ( for x being set holds
( x in the carrier of b1 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 & the mapping of b1 = the mapping of N | the carrier of b1 & ( for x being set holds
( x in the carrier of b2 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b2 = the InternalRel of N |_2 the carrier of b2 & the mapping of b2 = the mapping of N | the carrier of b2 holds
b1 = b2
proof
defpred S1[ set ] means ex y being Element of N st
( y = $1 & i <= y );
let A, B be strict NetStr over L; ::_thesis: ( ( for x being set holds
( x in the carrier of A iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of A = the InternalRel of N |_2 the carrier of A & the mapping of A = the mapping of N | the carrier of A & ( for x being set holds
( x in the carrier of B iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of B = the InternalRel of N |_2 the carrier of B & the mapping of B = the mapping of N | the carrier of B implies A = B )
assume that
A2: for x being set holds
( x in the carrier of A iff S1[x] ) and
A3: ( the InternalRel of A = the InternalRel of N |_2 the carrier of A & the mapping of A = the mapping of N | the carrier of A ) and
A4: for x being set holds
( x in the carrier of B iff S1[x] ) and
A5: ( the InternalRel of B = the InternalRel of N |_2 the carrier of B & the mapping of B = the mapping of N | the carrier of B ) ; ::_thesis: A = B
the carrier of A = the carrier of B from XBOOLE_0:sch_2(A2, A4);
hence A = B by A3, A5; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines | WAYBEL_9:def_7_:_
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N
for b4 being strict NetStr over L holds
( b4 = N | i iff ( ( for x being set holds
( x in the carrier of b4 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b4 = the InternalRel of N |_2 the carrier of b4 & the mapping of b4 = the mapping of N | the carrier of b4 ) );
theorem :: WAYBEL_9:12
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }
let N be non empty NetStr over L; ::_thesis: for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }
let i be Element of N; ::_thesis: the carrier of (N | i) = { y where y is Element of N : i <= y }
thus the carrier of (N | i) c= { y where y is Element of N : i <= y } :: according to XBOOLE_0:def_10 ::_thesis: { y where y is Element of N : i <= y } c= the carrier of (N | i)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the carrier of (N | i) or q in { y where y is Element of N : i <= y } )
assume q in the carrier of (N | i) ; ::_thesis: q in { y where y is Element of N : i <= y }
then ex y being Element of N st
( y = q & i <= y ) by Def7;
hence q in { y where y is Element of N : i <= y } ; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { y where y is Element of N : i <= y } or q in the carrier of (N | i) )
assume q in { y where y is Element of N : i <= y } ; ::_thesis: q in the carrier of (N | i)
then ex y being Element of N st
( q = y & i <= y ) ;
hence q in the carrier of (N | i) by Def7; ::_thesis: verum
end;
theorem Th13: :: WAYBEL_9:13
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) c= the carrier of N
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for i being Element of N holds the carrier of (N | i) c= the carrier of N
let N be non empty NetStr over L; ::_thesis: for i being Element of N holds the carrier of (N | i) c= the carrier of N
let i be Element of N; ::_thesis: the carrier of (N | i) c= the carrier of N
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (N | i) or x in the carrier of N )
assume x in the carrier of (N | i) ; ::_thesis: x in the carrier of N
then ex y being Element of N st
( y = x & i <= y ) by Def7;
hence x in the carrier of N ; ::_thesis: verum
end;
theorem Th14: :: WAYBEL_9:14
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds N | i is full SubNetStr of N
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for i being Element of N holds N | i is full SubNetStr of N
let N be non empty NetStr over L; ::_thesis: for i being Element of N holds N | i is full SubNetStr of N
let i be Element of N; ::_thesis: N | i is full SubNetStr of N
A1: the mapping of (N | i) = the mapping of N | the carrier of (N | i) by Def7;
the InternalRel of (N | i) = the InternalRel of N |_2 the carrier of (N | i) by Def7;
then A2: the InternalRel of (N | i) c= the InternalRel of N by XBOOLE_1:17;
the carrier of (N | i) c= the carrier of N by Th13;
then N | i is SubRelStr of N by A2, YELLOW_0:def_13;
then reconsider K = N | i as SubNetStr of N by A1, YELLOW_6:def_6;
the InternalRel of K = the InternalRel of N |_2 the carrier of K by Def7;
then K is full SubRelStr of N by YELLOW_0:def_14, YELLOW_6:def_6;
hence N | i is full SubNetStr of N by YELLOW_6:def_7; ::_thesis: verum
end;
registration
let L be non empty 1-sorted ;
let N be non empty reflexive NetStr over L;
let i be Element of N;
clusterN | i -> non empty reflexive strict ;
coherence
( not N | i is empty & N | i is reflexive )
proof
A1: i <= i ;
hence not N | i is empty by Def7; ::_thesis: N | i is reflexive
reconsider A = N | i as non empty strict NetStr over L by A1, Def7;
A is reflexive
proof
let x be Element of A; :: according to YELLOW_0:def_1 ::_thesis: x <= x
consider y being Element of N such that
A2: y = x and
i <= y by Def7;
( N | i is full SubNetStr of N & y <= y ) by Th14;
hence x <= x by A2, YELLOW_6:12; ::_thesis: verum
end;
hence N | i is reflexive ; ::_thesis: verum
end;
end;
registration
let L be non empty 1-sorted ;
let N be non empty directed NetStr over L;
let i be Element of N;
clusterN | i -> non empty strict ;
coherence
not N | i is empty
proof
ex z1 being Element of N st
( i <= z1 & i <= z1 ) by YELLOW_6:def_3;
hence not N | i is empty by Def7; ::_thesis: verum
end;
end;
registration
let L be non empty 1-sorted ;
let N be non empty reflexive antisymmetric NetStr over L;
let i be Element of N;
clusterN | i -> antisymmetric strict ;
coherence
N | i is antisymmetric
proof
let x, y be Element of (N | i); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
assume A1: ( x <= y & y <= x ) ; ::_thesis: x = y
consider y1 being Element of N such that
A2: y1 = y and
i <= y1 by Def7;
consider x1 being Element of N such that
A3: x1 = x and
i <= x1 by Def7;
N | i is SubNetStr of N by Th14;
then ( x1 <= y1 & y1 <= x1 ) by A1, A3, A2, YELLOW_6:11;
hence x = y by A3, A2, YELLOW_0:def_3; ::_thesis: verum
end;
end;
registration
let L be non empty 1-sorted ;
let N be non empty antisymmetric directed NetStr over L;
let i be Element of N;
clusterN | i -> antisymmetric strict ;
coherence
N | i is antisymmetric
proof
let x, y be Element of (N | i); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
assume A1: ( x <= y & y <= x ) ; ::_thesis: x = y
consider y1 being Element of N such that
A2: y1 = y and
i <= y1 by Def7;
consider x1 being Element of N such that
A3: x1 = x and
i <= x1 by Def7;
N | i is SubNetStr of N by Th14;
then ( x1 <= y1 & y1 <= x1 ) by A1, A3, A2, YELLOW_6:11;
hence x = y by A3, A2, YELLOW_0:def_3; ::_thesis: verum
end;
end;
registration
let L be non empty 1-sorted ;
let N be non empty reflexive transitive NetStr over L;
let i be Element of N;
clusterN | i -> transitive strict ;
coherence
N | i is transitive
proof
let x, y, z be Element of (N | i); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
consider z1 being Element of N such that
A3: z1 = z and
i <= z1 by Def7;
consider x1 being Element of N such that
A4: x1 = x and
i <= x1 by Def7;
consider y1 being Element of N such that
A5: y1 = y and
i <= y1 by Def7;
A6: N | i is full SubNetStr of N by Th14;
then A7: y1 <= z1 by A2, A5, A3, YELLOW_6:11;
x1 <= y1 by A1, A6, A4, A5, YELLOW_6:11;
then x1 <= z1 by A7, YELLOW_0:def_2;
hence x <= z by A6, A4, A3, YELLOW_6:12; ::_thesis: verum
end;
end;
registration
let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
clusterN | i -> transitive strict directed ;
coherence
( N | i is transitive & N | i is directed )
proof
thus N | i is transitive ::_thesis: N | i is directed
proof
let x, y, z be Element of (N | i); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
consider z1 being Element of N such that
A3: z1 = z and
i <= z1 by Def7;
consider x1 being Element of N such that
A4: x1 = x and
i <= x1 by Def7;
consider y1 being Element of N such that
A5: y1 = y and
i <= y1 by Def7;
A6: N | i is full SubNetStr of N by Th14;
then A7: y1 <= z1 by A2, A5, A3, YELLOW_6:11;
x1 <= y1 by A1, A6, A4, A5, YELLOW_6:11;
then x1 <= z1 by A7, YELLOW_0:def_2;
hence x <= z by A6, A4, A3, YELLOW_6:12; ::_thesis: verum
end;
for x, y being Element of (N | i) ex z being Element of (N | i) st
( x <= z & y <= z )
proof
let x, y be Element of (N | i); ::_thesis: ex z being Element of (N | i) st
( x <= z & y <= z )
consider x1 being Element of N such that
A8: x1 = x and
A9: i <= x1 by Def7;
consider y1 being Element of N such that
A10: y1 = y and
i <= y1 by Def7;
consider z1 being Element of N such that
A11: x1 <= z1 and
A12: y1 <= z1 by YELLOW_6:def_3;
i <= z1 by A9, A11, YELLOW_0:def_2;
then reconsider z = z1 as Element of (N | i) by Def7;
take z ; ::_thesis: ( x <= z & y <= z )
N | i is full SubNetStr of N by Th14;
hence ( x <= z & y <= z ) by A8, A10, A11, A12, YELLOW_6:12; ::_thesis: verum
end;
hence N | i is directed by YELLOW_6:def_3; ::_thesis: verum
end;
end;
theorem :: WAYBEL_9:15
for L being non empty 1-sorted
for N being non empty reflexive NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty reflexive NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let N be non empty reflexive NetStr over L; ::_thesis: for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let i, x be Element of N; ::_thesis: for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let x1 be Element of (N | i); ::_thesis: ( x = x1 implies N . x = (N | i) . x1 )
assume x = x1 ; ::_thesis: N . x = (N | i) . x1
hence N . x = ( the mapping of N | the carrier of (N | i)) . x1 by FUNCT_1:49
.= (N | i) . x1 by Def7 ;
::_thesis: verum
end;
theorem Th16: :: WAYBEL_9:16
for L being non empty 1-sorted
for N being non empty directed NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty directed NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let N be non empty directed NetStr over L; ::_thesis: for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let i, x be Element of N; ::_thesis: for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
let x1 be Element of (N | i); ::_thesis: ( x = x1 implies N . x = (N | i) . x1 )
assume x = x1 ; ::_thesis: N . x = (N | i) . x1
hence N . x = ( the mapping of N | the carrier of (N | i)) . x1 by FUNCT_1:49
.= (N | i) . x1 by Def7 ;
::_thesis: verum
end;
theorem Th17: :: WAYBEL_9:17
for L being non empty 1-sorted
for N being net of L
for i being Element of N holds N | i is subnet of N
proof
let L be non empty 1-sorted ; ::_thesis: for N being net of L
for i being Element of N holds N | i is subnet of N
let N be net of L; ::_thesis: for i being Element of N holds N | i is subnet of N
let i be Element of N; ::_thesis: N | i is subnet of N
reconsider A = N | i as net of L ;
A1: the carrier of A c= the carrier of N by Th13;
A is subnet of N
proof
reconsider f = id the carrier of A as Function of A,N by A1, FUNCT_2:7;
take f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of A = the mapping of N * f & ( for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st
for b3 being Element of the carrier of A holds
( not b2 <= b3 or b1 <= f . b3 ) ) )
for x being set st x in the carrier of A holds
the mapping of A . x = ( the mapping of N * f) . x
proof
let x be set ; ::_thesis: ( x in the carrier of A implies the mapping of A . x = ( the mapping of N * f) . x )
assume A2: x in the carrier of A ; ::_thesis: the mapping of A . x = ( the mapping of N * f) . x
thus the mapping of A . x = ( the mapping of N | the carrier of A) . x by Def7
.= the mapping of N . x by A2, FUNCT_1:49
.= the mapping of N . (f . x) by A2, FUNCT_1:18
.= ( the mapping of N * f) . x by A2, FUNCT_2:15 ; ::_thesis: verum
end;
hence the mapping of A = the mapping of N * f by FUNCT_2:12; ::_thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st
for b3 being Element of the carrier of A holds
( not b2 <= b3 or b1 <= f . b3 )
let m be Element of N; ::_thesis: ex b1 being Element of the carrier of A st
for b2 being Element of the carrier of A holds
( not b1 <= b2 or m <= f . b2 )
consider z being Element of N such that
A3: i <= z and
A4: m <= z by YELLOW_6:def_3;
reconsider n = z as Element of A by A3, Def7;
take n ; ::_thesis: for b1 being Element of the carrier of A holds
( not n <= b1 or m <= f . b1 )
let p be Element of A; ::_thesis: ( not n <= p or m <= f . p )
assume A5: n <= p ; ::_thesis: m <= f . p
p in the carrier of A ;
then reconsider p1 = p as Element of N by A1;
A is SubNetStr of N by Th14;
then z <= p1 by A5, YELLOW_6:11;
then m <= p1 by A4, YELLOW_0:def_2;
hence m <= f . p by FUNCT_1:18; ::_thesis: verum
end;
hence N | i is subnet of N ; ::_thesis: verum
end;
registration
let T be non empty 1-sorted ;
let N be net of T;
cluster non empty transitive strict directed for subnet of N;
existence
ex b1 being subnet of N st b1 is strict
proof
set A = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #);
A1: RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) #) = RelStr(# the carrier of N, the InternalRel of N #) ;
[#] N is directed by WAYBEL_0:def_6;
then [#] NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is directed by A1, WAYBEL_0:3;
then reconsider A = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as net of T by A1, WAYBEL_0:def_6, WAYBEL_8:13;
A is subnet of N
proof
reconsider f = id N as Function of A,N ;
take f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of A = the mapping of N * f & ( for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st
for b3 being Element of the carrier of A holds
( not b2 <= b3 or b1 <= f . b3 ) ) )
thus the mapping of A = the mapping of N * f by FUNCT_2:17; ::_thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st
for b3 being Element of the carrier of A holds
( not b2 <= b3 or b1 <= f . b3 )
let m be Element of N; ::_thesis: ex b1 being Element of the carrier of A st
for b2 being Element of the carrier of A holds
( not b1 <= b2 or m <= f . b2 )
reconsider n = m as Element of A ;
take n ; ::_thesis: for b1 being Element of the carrier of A holds
( not n <= b1 or m <= f . b1 )
let p be Element of A; ::_thesis: ( not n <= p or m <= f . p )
assume A2: n <= p ; ::_thesis: m <= f . p
p = f . p by FUNCT_1:18;
hence m <= f . p by A1, A2, YELLOW_0:1; ::_thesis: verum
end;
then reconsider A = A as subnet of N ;
take A ; ::_thesis: A is strict
thus A is strict ; ::_thesis: verum
end;
end;
definition
let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
:: original: |
redefine funcN | i -> strict subnet of N;
coherence
N | i is strict subnet of N by Th17;
end;
definition
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be NetStr over S;
funcf * N -> strict NetStr over T means :Def8: :: WAYBEL_9:def 8
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = f * the mapping of N );
existence
ex b1 being strict NetStr over T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = f * the mapping of N )
proof
take NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) = f * the mapping of N )
thus ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,(f * the mapping of N) #) = f * the mapping of N ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict NetStr over T st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = f * the mapping of N & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = f * the mapping of N holds
b1 = b2 ;
end;
:: deftheorem Def8 defines * WAYBEL_9:def_8_:_
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T
for N being NetStr over S
for b5 being strict NetStr over T holds
( b5 = f * N iff ( RelStr(# the carrier of b5, the InternalRel of b5 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b5 = f * the mapping of N ) );
registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be non empty NetStr over S;
clusterf * N -> non empty strict ;
coherence
not f * N is empty
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8;
hence not f * N is empty ; ::_thesis: verum
end;
end;
registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be reflexive NetStr over S;
clusterf * N -> reflexive strict ;
coherence
f * N is reflexive
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8;
hence the InternalRel of (f * N) is_reflexive_in the carrier of (f * N) by ORDERS_2:def_2; :: according to ORDERS_2:def_2 ::_thesis: verum
end;
end;
registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be antisymmetric NetStr over S;
clusterf * N -> antisymmetric strict ;
coherence
f * N is antisymmetric
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8;
then the InternalRel of (f * N) is_antisymmetric_in the carrier of (f * N) by ORDERS_2:def_4;
hence f * N is antisymmetric by ORDERS_2:def_4; ::_thesis: verum
end;
end;
registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be transitive NetStr over S;
clusterf * N -> transitive strict ;
coherence
f * N is transitive
proof
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by Def8;
then the InternalRel of (f * N) is_transitive_in the carrier of (f * N) by ORDERS_2:def_3;
hence f * N is transitive by ORDERS_2:def_3; ::_thesis: verum
end;
end;
registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be directed NetStr over S;
clusterf * N -> strict directed ;
coherence
f * N is directed
proof
( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) & [#] N is directed ) by Def8, WAYBEL_0:def_6;
hence [#] (f * N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
theorem Th18: :: WAYBEL_9:18
for L being non empty RelStr
for N being non empty NetStr over L
for x being Element of L holds (x "/\") * N = x "/\" N
proof
let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L
for x being Element of L holds (x "/\") * N = x "/\" N
let N be non empty NetStr over L; ::_thesis: for x being Element of L holds (x "/\") * N = x "/\" N
let x be Element of L; ::_thesis: (x "/\") * N = x "/\" N
set n = the mapping of N;
A1: RelStr(# the carrier of ((x "/\") * N), the InternalRel of ((x "/\") * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def8
.= RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3 ;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def_3;
then reconsider f2 = the mapping of (x "/\" N) as Function of the carrier of N, the carrier of L ;
A3: for c being Element of N holds ((x "/\") * the mapping of N) . c = f2 . c
proof
let c be Element of N; ::_thesis: ((x "/\") * the mapping of N) . c = f2 . c
consider y being Element of L such that
A4: y = the mapping of N . c and
A5: f2 . c = x "/\" y by A2, WAYBEL_2:def_3;
thus ((x "/\") * the mapping of N) . c = (x "/\") . y by A4, FUNCT_2:15
.= f2 . c by A5, WAYBEL_1:def_18 ; ::_thesis: verum
end;
the mapping of ((x "/\") * N) = (x "/\") * the mapping of N by Def8
.= the mapping of (x "/\" N) by A3, FUNCT_2:63 ;
hence (x "/\") * N = x "/\" N by A1; ::_thesis: verum
end;
begin
theorem :: WAYBEL_9:19
for S, T being TopStruct
for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds
G is open
proof
let S, T be TopStruct ; ::_thesis: for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds
G is open
let F be Subset-Family of S; ::_thesis: for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds
G is open
let G be Subset-Family of T; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open implies G is open )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: ( F = G & F is open ) ; ::_thesis: G is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in G or P is open )
assume A3: P in G ; ::_thesis: P is open
reconsider R = P as Subset of S by A1;
R is open by A2, A3, TOPS_2:def_1;
hence P in the topology of T by A1, PRE_TOPC:def_2; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
theorem :: WAYBEL_9:20
for S, T being TopStruct
for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed
proof
let S, T be TopStruct ; ::_thesis: for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed
let F be Subset-Family of S; ::_thesis: for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed
let G be Subset-Family of T; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed implies G is closed )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: ( F = G & F is closed ) ; ::_thesis: G is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in G or P is closed )
assume A3: P in G ; ::_thesis: P is closed
reconsider R = P as Subset of S by A1;
R is closed by A2, A3, TOPS_2:def_2;
then ([#] S) \ R is open by PRE_TOPC:def_3;
hence ([#] T) \ P in the topology of T by A1, PRE_TOPC:def_2; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum
end;
definition
attrc1 is strict ;
struct TopRelStr -> TopStruct , RelStr ;
aggrTopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;
end;
registration
let A be non empty set ;
let R be Relation of A,A;
let T be Subset-Family of A;
cluster TopRelStr(# A,R,T #) -> non empty ;
coherence
not TopRelStr(# A,R,T #) is empty ;
end;
registration
let x be set ;
let R be Relation of {x};
let T be Subset-Family of {x};
cluster TopRelStr(# {x},R,T #) -> 1 -element ;
coherence
TopRelStr(# {x},R,T #) is 1 -element
proof
thus the carrier of TopRelStr(# {x},R,T #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;
registration
let X be set ;
let O be Order of X;
let T be Subset-Family of X;
cluster TopRelStr(# X,O,T #) -> reflexive transitive antisymmetric ;
coherence
( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric )
proof
set A = TopRelStr(# X,O,T #);
A1: field the InternalRel of TopRelStr(# X,O,T #) = the carrier of TopRelStr(# X,O,T #) by ORDERS_1:12;
then A2: the InternalRel of TopRelStr(# X,O,T #) is_antisymmetric_in the carrier of TopRelStr(# X,O,T #) by RELAT_2:def_12;
( the InternalRel of TopRelStr(# X,O,T #) is_reflexive_in the carrier of TopRelStr(# X,O,T #) & the InternalRel of TopRelStr(# X,O,T #) is_transitive_in the carrier of TopRelStr(# X,O,T #) ) by A1, RELAT_2:def_9, RELAT_2:def_16;
hence ( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric ) by A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum
end;
end;
Lm4: for tau being Subset-Family of {0}
for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds
( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
proof
let tau be Subset-Family of {0}; ::_thesis: for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds
( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
let r be Relation of {0}; ::_thesis: ( tau = {{},{0}} & r = {[0,0]} implies ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) )
assume that
A1: tau = {{},{0}} and
A2: r = {[0,0]} ; ::_thesis: ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
set T = TopRelStr(# {0},r,tau #);
thus TopRelStr(# {0},r,tau #) is reflexive ::_thesis: ( TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
proof
let x be Element of TopRelStr(# {0},r,tau #); :: according to YELLOW_0:def_1 ::_thesis: x <= x
x = 0 by TARSKI:def_1;
then [x,x] in {[0,0]} by TARSKI:def_1;
hence x <= x by A2, ORDERS_2:def_5; ::_thesis: verum
end;
the topology of TopRelStr(# {0},r,tau #) = bool the carrier of TopRelStr(# {0},r,tau #) by A1, ZFMISC_1:24;
hence TopRelStr(# {0},r,tau #) is discrete by TDLAT_3:def_1; ::_thesis: ( TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
thus ( TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) ; ::_thesis: verum
end;
registration
cluster finite 1 -element discrete reflexive strict for TopRelStr ;
existence
ex b1 being TopRelStr st
( b1 is reflexive & b1 is discrete & b1 is strict & b1 is finite & b1 is 1 -element )
proof
0 in {0} by TARSKI:def_1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
{{},{0}} = bool {0} by ZFMISC_1:24;
then reconsider tau = {{},{0}} as Subset-Family of {0} ;
take TopRelStr(# {0},r,tau #) ; ::_thesis: ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is strict & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
thus ( TopRelStr(# {0},r,tau #) is reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is strict & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element ) by Lm4; ::_thesis: verum
end;
end;
definition
mode TopLattice is TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr ;
end;
registration
cluster non empty finite 1 -element TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is strict & b1 is discrete & b1 is finite & b1 is compact & b1 is Hausdorff & b1 is 1 -element )
proof
reconsider C = bool {0} as Subset-Family of {0} ;
0 in {0} by TARSKI:def_1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
{{},{0}} = bool {0} by ZFMISC_1:24;
then reconsider A = TopRelStr(# {0},r,C #) as finite 1 -element discrete reflexive TopRelStr by Lm4;
reconsider A = A as TopLattice ;
take A ; ::_thesis: ( A is strict & A is discrete & A is finite & A is compact & A is Hausdorff & A is 1 -element )
thus ( A is strict & A is discrete & A is finite ) ; ::_thesis: ( A is compact & A is Hausdorff & A is 1 -element )
thus A is compact ; ::_thesis: ( A is Hausdorff & A is 1 -element )
thus A is Hausdorff ::_thesis: A is 1 -element
proof
let p, q be Point of A; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of A) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A1: not p = q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of A) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
p = 0 by TARSKI:def_1;
hence ex b1, b2 being Element of K10( the carrier of A) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A1, TARSKI:def_1; ::_thesis: verum
end;
thus A is 1 -element ; ::_thesis: verum
end;
end;
registration
let T be non empty Hausdorff TopSpace;
cluster non empty -> non empty Hausdorff for SubSpace of T;
coherence
for b1 being non empty SubSpace of T holds b1 is Hausdorff ;
end;
theorem Th21: :: WAYBEL_9:21
for T being non empty TopSpace
for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
let p be Point of T; ::_thesis: for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
let A be Element of (OpenNeighborhoods p); ::_thesis: A is a_neighborhood of p
ex W being Subset of T st
( W = A & p in W & W is open ) by YELLOW_6:29;
hence A is a_neighborhood of p by CONNSP_2:3; ::_thesis: verum
end;
theorem Th22: :: WAYBEL_9:22
for T being non empty TopSpace
for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
let p be Point of T; ::_thesis: for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
let A, B be Element of (OpenNeighborhoods p); ::_thesis: A /\ B is Element of (OpenNeighborhoods p)
consider W being Subset of T such that
A1: W = A and
A2: ( p in W & W is open ) by YELLOW_6:29;
consider X being Subset of T such that
A3: X = B and
A4: ( p in X & X is open ) by YELLOW_6:29;
( p in A /\ B & W /\ X is open ) by A1, A2, A3, A4, XBOOLE_0:def_4;
hence A /\ B is Element of (OpenNeighborhoods p) by A1, A3, YELLOW_6:30; ::_thesis: verum
end;
theorem :: WAYBEL_9:23
for T being non empty TopSpace
for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)
let p be Point of T; ::_thesis: for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)
let A, B be Element of (OpenNeighborhoods p); ::_thesis: A \/ B is Element of (OpenNeighborhoods p)
consider W being Subset of T such that
A1: W = A and
A2: p in W and
A3: W is open by YELLOW_6:29;
A4: p in A \/ B by A1, A2, XBOOLE_0:def_3;
consider X being Subset of T such that
A5: X = B and
p in X and
A6: X is open by YELLOW_6:29;
W \/ X is open by A3, A6;
hence A \/ B is Element of (OpenNeighborhoods p) by A1, A5, A4, YELLOW_6:30; ::_thesis: verum
end;
theorem Th24: :: WAYBEL_9:24
for T being non empty TopSpace
for p being Element of T
for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S
proof
let T be non empty TopSpace; ::_thesis: for p being Element of T
for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S
let p be Element of T; ::_thesis: for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S
let N be net of T; ::_thesis: ( p in Lim N implies for S being Subset of T st S = rng the mapping of N holds
p in Cl S )
assume A1: p in Lim N ; ::_thesis: for S being Subset of T st S = rng the mapping of N holds
p in Cl S
let S be Subset of T; ::_thesis: ( S = rng the mapping of N implies p in Cl S )
assume S = rng the mapping of N ; ::_thesis: p in Cl S
then A2: N is_eventually_in S by Th8;
for G being Subset of T st G is open & p in G holds
S meets G
proof
let G be Subset of T; ::_thesis: ( G is open & p in G implies S meets G )
assume that
A3: G is open and
A4: p in G ; ::_thesis: S meets G
G = Int G by A3, TOPS_1:23;
then reconsider V = G as a_neighborhood of p by A4, CONNSP_2:def_1;
N is_eventually_in V by A1, YELLOW_6:def_15;
hence S meets G by A2, YELLOW_6:17; ::_thesis: verum
end;
hence p in Cl S by PRE_TOPC:def_7; ::_thesis: verum
end;
theorem Th25: :: WAYBEL_9:25
for T being Hausdorff TopLattice
for N being convergent net of T
for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)
proof
let T be Hausdorff TopLattice; ::_thesis: for N being convergent net of T
for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)
let N be convergent net of T; ::_thesis: for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)
let f be Function of T,T; ::_thesis: ( f is continuous implies f . (lim N) in Lim (f * N) )
assume A1: f is continuous ; ::_thesis: f . (lim N) in Lim (f * N)
for V being a_neighborhood of f . (lim N) holds f * N is_eventually_in V
proof
let V be a_neighborhood of f . (lim N); ::_thesis: f * N is_eventually_in V
A2: dom f = the carrier of T by FUNCT_2:def_1;
consider O being a_neighborhood of lim N such that
A3: f .: O c= V by A1, BORSUK_1:def_1;
lim N in Lim N by YELLOW_6:def_17;
then N is_eventually_in O by YELLOW_6:def_15;
then consider s0 being Element of N such that
A4: for j being Element of N st s0 <= j holds
N . j in O by WAYBEL_0:def_11;
A5: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def8;
then reconsider s1 = s0 as Element of (f * N) ;
take s1 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (f * N) holds
( not s1 <= b1 or (f * N) . b1 in V )
let j1 be Element of (f * N); ::_thesis: ( not s1 <= j1 or (f * N) . j1 in V )
assume A6: s1 <= j1 ; ::_thesis: (f * N) . j1 in V
reconsider j = j1 as Element of N by A5;
N . j in O by A4, A5, A6, YELLOW_0:1;
then A7: f . (N . j) in f .: O by A2, FUNCT_1:def_6;
A8: the carrier of (f * N) = dom the mapping of N by A5, FUNCT_2:def_1;
(f * N) . j1 = (f * the mapping of N) . j1 by Def8
.= f . (N . j) by A8, FUNCT_1:13 ;
hence (f * N) . j1 in V by A3, A7; ::_thesis: verum
end;
hence f . (lim N) in Lim (f * N) by YELLOW_6:def_15; ::_thesis: verum
end;
theorem Th26: :: WAYBEL_9:26
for T being Hausdorff TopLattice
for N being convergent net of T
for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)
proof
let T be Hausdorff TopLattice; ::_thesis: for N being convergent net of T
for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)
let N be convergent net of T; ::_thesis: for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)
let x be Element of T; ::_thesis: ( x "/\" is continuous implies x "/\" (lim N) in Lim (x "/\" N) )
assume A1: x "/\" is continuous ; ::_thesis: x "/\" (lim N) in Lim (x "/\" N)
x "/\" (lim N) = (x "/\") . (lim N) by WAYBEL_1:def_18;
then x "/\" (lim N) in Lim ((x "/\") * N) by A1, Th25;
hence x "/\" (lim N) in Lim (x "/\" N) by Th18; ::_thesis: verum
end;
theorem Th27: :: WAYBEL_9:27
for S being Hausdorff TopLattice
for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds
uparrow x is closed
proof
let S be Hausdorff TopLattice; ::_thesis: for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds
uparrow x is closed
let x be Element of S; ::_thesis: ( ( for a being Element of S holds a "/\" is continuous ) implies uparrow x is closed )
assume for a being Element of S holds a "/\" is continuous ; ::_thesis: uparrow x is closed
then A1: x "/\" is continuous ;
( (x "/\") " {x} = uparrow x & {x} is closed ) by Th7, PCOMPS_1:7;
hence uparrow x is closed by A1, PRE_TOPC:def_6; ::_thesis: verum
end;
theorem Th28: :: WAYBEL_9:28
for S being Hausdorff compact TopLattice
for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds
downarrow x is closed
proof
let S be Hausdorff compact TopLattice; ::_thesis: for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds
downarrow x is closed
let b be Element of S; ::_thesis: ( ( for b being Element of S holds b "/\" is continuous ) implies downarrow b is closed )
assume for a being Element of S holds a "/\" is continuous ; ::_thesis: downarrow b is closed
then A1: b "/\" is continuous ;
set g1 = (rng (b "/\")) |` (b "/\");
A2: (rng (b "/\")) |` (b "/\") = b "/\" by RELAT_1:94;
A3: dom (b "/\") = the carrier of S by FUNCT_2:def_1;
A4: {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } by YELLOW_4:42;
A5: rng (b "/\") = {b} "/\" ([#] S)
proof
thus rng (b "/\") c= {b} "/\" ([#] S) :: according to XBOOLE_0:def_10 ::_thesis: {b} "/\" ([#] S) c= rng (b "/\")
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng (b "/\") or q in {b} "/\" ([#] S) )
assume q in rng (b "/\") ; ::_thesis: q in {b} "/\" ([#] S)
then consider x being set such that
A6: x in dom (b "/\") and
A7: (b "/\") . x = q by FUNCT_1:def_3;
reconsider x1 = x as Element of S by A6;
q = b "/\" x1 by A7, WAYBEL_1:def_18;
hence q in {b} "/\" ([#] S) by A4; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {b} "/\" ([#] S) or q in rng (b "/\") )
assume q in {b} "/\" ([#] S) ; ::_thesis: q in rng (b "/\")
then consider y being Element of S such that
A8: q = b "/\" y and
y in [#] S by A4;
q = (b "/\") . y by A8, WAYBEL_1:def_18;
hence q in rng (b "/\") by A3, FUNCT_1:def_3; ::_thesis: verum
end;
then rng ((rng (b "/\")) |` (b "/\")) = {b} "/\" ([#] S) by RELAT_1:94
.= [#] (S | (rng (b "/\"))) by A5, PRE_TOPC:def_5
.= the carrier of (S | (rng (b "/\"))) ;
then reconsider g1 = (rng (b "/\")) |` (b "/\") as Function of S,(S | (rng (b "/\"))) by A2, A3, FUNCT_2:1;
rng g1 = {b} "/\" ([#] S) by A5, RELAT_1:94
.= [#] (S | ({b} "/\" ([#] S))) by PRE_TOPC:def_5 ;
then S | ({b} "/\" ([#] S)) is compact by A1, A2, A5, COMPTS_1:14, PRE_TOPC:27;
then {b} "/\" ([#] S) is compact by COMPTS_1:3;
hence downarrow b is closed by Th5; ::_thesis: verum
end;
begin
definition
let T be non empty TopSpace;
let N be non empty NetStr over T;
let p be Point of T;
predp is_a_cluster_point_of N means :Def9: :: WAYBEL_9:def 9
for O being a_neighborhood of p holds N is_often_in O;
end;
:: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def_9_:_
for T being non empty TopSpace
for N being non empty NetStr over T
for p being Point of T holds
( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O );
theorem :: WAYBEL_9:29
for L being non empty TopSpace
for N being net of L
for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N
proof
let L be non empty TopSpace; ::_thesis: for N being net of L
for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N
let N be net of L; ::_thesis: for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N
let c be Point of L; ::_thesis: ( c in Lim N implies c is_a_cluster_point_of N )
assume A1: c in Lim N ; ::_thesis: c is_a_cluster_point_of N
let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in O
N is_eventually_in O by A1, YELLOW_6:def_15;
hence N is_often_in O by YELLOW_6:19; ::_thesis: verum
end;
theorem Th30: :: WAYBEL_9:30
for T being non empty Hausdorff compact TopSpace
for N being net of T ex c being Point of T st c is_a_cluster_point_of N
proof
let T be non empty Hausdorff compact TopSpace; ::_thesis: for N being net of T ex c being Point of T st c is_a_cluster_point_of N
let N be net of T; ::_thesis: ex c being Point of T st c is_a_cluster_point_of N
defpred S1[ set , set ] means ex X being Subset of T ex a being Element of N st
( a = $1 & X = { (N . j) where j is Element of N : a <= j } & $2 = Cl X );
A1: for e being Element of N ex u being Subset of T st S1[e,u]
proof
let e be Element of N; ::_thesis: ex u being Subset of T st S1[e,u]
reconsider a = e as Element of N ;
{ (N . j) where j is Element of N : a <= j } c= the carrier of T
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (N . j) where j is Element of N : a <= j } or q in the carrier of T )
assume q in { (N . j) where j is Element of N : a <= j } ; ::_thesis: q in the carrier of T
then ex j being Element of N st
( q = N . j & a <= j ) ;
hence q in the carrier of T ; ::_thesis: verum
end;
then reconsider X = { (N . j) where j is Element of N : a <= j } as Subset of the carrier of T ;
take Cl X ; ::_thesis: S1[e, Cl X]
take X ; ::_thesis: ex a being Element of N st
( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X )
take a ; ::_thesis: ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X )
thus ( a = e & X = { (N . j) where j is Element of N : a <= j } & Cl X = Cl X ) ; ::_thesis: verum
end;
consider F being Function of the carrier of N,(bool the carrier of T) such that
A2: for e being Element of N holds S1[e,F . e] from FUNCT_2:sch_3(A1);
reconsider RF = rng F as Subset-Family of T ;
A3: dom F = the carrier of N by FUNCT_2:def_1;
A4: RF is centered
proof
thus RF <> {} by A3, RELAT_1:42; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds
( b1 = {} or not b1 c= RF or not b1 is finite or not meet b1 = {} )
defpred S2[ set , set ] means ex i being Element of N ex h, Ch being Subset of T st
( i = $2 & Ch = $1 & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h );
set J = { i where i is Element of N : ex h, Ch being Subset of T st
( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } ;
let H be set ; ::_thesis: ( H = {} or not H c= RF or not H is finite or not meet H = {} )
assume that
A5: H <> {} and
A6: H c= RF and
A7: H is finite ; ::_thesis: not meet H = {}
reconsider H1 = H as non empty set by A5;
set e = the Element of H1;
the Element of H1 in RF by A6, TARSKI:def_3;
then consider x being set such that
A8: x in dom F and
the Element of H1 = F . x by FUNCT_1:def_3;
reconsider x = x as Element of N by A8;
consider X being Subset of T, a being Element of N such that
a = x and
A9: ( X = { (N . j) where j is Element of N : a <= j } & F . x = Cl X ) by A2;
a in { i where i is Element of N : ex h, Ch being Subset of T st
( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } by A9;
then reconsider J = { i where i is Element of N : ex h, Ch being Subset of T st
( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) } as non empty set ;
A10: for e being Element of H1 ex u being Element of J st S2[e,u]
proof
let e be Element of H1; ::_thesis: ex u being Element of J st S2[e,u]
e in RF by A6, TARSKI:def_3;
then consider x being set such that
A11: x in dom F and
A12: e = F . x by FUNCT_1:def_3;
reconsider x = x as Element of N by A11;
consider X being Subset of T, a being Element of N such that
A13: a = x and
A14: X = { (N . j) where j is Element of N : a <= j } and
A15: F . x = Cl X by A2;
a in J by A14, A15;
then reconsider a = a as Element of J ;
take u = a; ::_thesis: S2[e,u]
take i = x; ::_thesis: ex h, Ch being Subset of T st
( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
take h = X; ::_thesis: ex Ch being Subset of T st
( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
take Ch = Cl X; ::_thesis: ( i = u & Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
thus i = u by A13; ::_thesis: ( Ch = e & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
thus Ch = e by A12, A15; ::_thesis: ( h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h )
thus h = { (N . j) where j is Element of N : i <= j } by A13, A14; ::_thesis: Ch = Cl h
thus Ch = Cl h ; ::_thesis: verum
end;
consider Q being Function of H1,J such that
A16: for e being Element of H1 holds S2[e,Q . e] from FUNCT_2:sch_3(A10);
rng Q c= [#] N
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng Q or q in [#] N )
assume q in rng Q ; ::_thesis: q in [#] N
then consider x being set such that
A17: x in dom Q and
A18: Q . x = q by FUNCT_1:def_3;
reconsider x = x as Element of H1 by A17;
ex i being Element of N ex h, Ch being Subset of T st
( i = Q . x & Ch = x & h = { (N . j) where j is Element of N : i <= j } & Ch = Cl h ) by A16;
hence q in [#] N by A18; ::_thesis: verum
end;
then reconsider RQ = rng Q as Subset of ([#] N) ;
A19: ( not [#] N is empty & [#] N is directed ) by WAYBEL_0:def_6;
dom Q = H by FUNCT_2:def_1;
then rng Q is finite by A7, FINSET_1:8;
then consider i0 being Element of N such that
i0 in [#] N and
A20: i0 is_>=_than RQ by A19, WAYBEL_0:1;
for Y being set st Y in H holds
N . i0 in Y
proof
let Y be set ; ::_thesis: ( Y in H implies N . i0 in Y )
assume A21: Y in H ; ::_thesis: N . i0 in Y
then consider i being Element of N, h, Ch being Subset of T such that
A22: i = Q . Y and
A23: Ch = Y and
A24: h = { (N . j) where j is Element of N : i <= j } and
A25: Ch = Cl h by A16;
Y in dom Q by A21, FUNCT_2:def_1;
then i in rng Q by A22, FUNCT_1:def_3;
then i <= i0 by A20, LATTICE3:def_9;
then A26: N . i0 in h by A24;
h c= Cl h by PRE_TOPC:18;
hence N . i0 in Y by A23, A25, A26; ::_thesis: verum
end;
hence not meet H = {} by A5, SETFAM_1:def_1; ::_thesis: verum
end;
RF is closed
proof
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in RF or P is closed )
assume P in RF ; ::_thesis: P is closed
then consider x being set such that
A27: x in dom F and
A28: F . x = P by FUNCT_1:def_3;
reconsider x = x as Element of N by A27;
ex X being Subset of T ex a being Element of N st
( a = x & X = { (N . j) where j is Element of N : a <= j } & F . x = Cl X ) by A2;
then P = Cl P by A28;
hence P is closed ; ::_thesis: verum
end;
then meet RF <> {} by A4, COMPTS_1:4;
then consider c being set such that
A29: c in meet RF by XBOOLE_0:def_1;
reconsider c = c as Point of T by A29;
take c ; ::_thesis: c is_a_cluster_point_of N
assume not c is_a_cluster_point_of N ; ::_thesis: contradiction
then consider O being a_neighborhood of c such that
A30: not N is_often_in O by Def9;
N is_eventually_in the carrier of T \ O by A30, WAYBEL_0:10;
then consider s0 being Element of N such that
A31: for j being Element of N st s0 <= j holds
N . j in the carrier of T \ O by WAYBEL_0:def_11;
consider Y being Subset of T, a being Element of N such that
A32: ( a = s0 & Y = { (N . j) where j is Element of N : a <= j } ) and
A33: F . s0 = Cl Y by A2;
Cl Y in RF by A3, A33, FUNCT_1:def_3;
then A34: c in Cl Y by A29, SETFAM_1:def_1;
{} = O /\ Y
proof
thus {} c= O /\ Y by XBOOLE_1:2; :: according to XBOOLE_0:def_10 ::_thesis: O /\ Y c= {}
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O /\ Y or q in {} )
assume A35: q in O /\ Y ; ::_thesis: q in {}
q in Y by A35, XBOOLE_0:def_4;
then consider j being Element of N such that
A36: q = N . j and
A37: s0 <= j by A32;
assume not q in {} ; ::_thesis: contradiction
N . j in the carrier of T \ O by A31, A37;
then not N . j in O by XBOOLE_0:def_5;
hence contradiction by A35, A36, XBOOLE_0:def_4; ::_thesis: verum
end;
then O misses Y by XBOOLE_0:def_7;
then A38: Int O misses Y by TOPS_1:16, XBOOLE_1:63;
( Int O is open & c in Int O ) by CONNSP_2:def_1;
hence contradiction by A34, A38, PRE_TOPC:def_7; ::_thesis: verum
end;
theorem Th31: :: WAYBEL_9:31
for L being non empty TopSpace
for N being net of L
for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
proof
let L be non empty TopSpace; ::_thesis: for N being net of L
for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
let N be net of L; ::_thesis: for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
let M be subnet of N; ::_thesis: for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
let c be Point of L; ::_thesis: ( c is_a_cluster_point_of M implies c is_a_cluster_point_of N )
assume A1: c is_a_cluster_point_of M ; ::_thesis: c is_a_cluster_point_of N
let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in O
M is_often_in O by A1, Def9;
hence N is_often_in O by YELLOW_6:18; ::_thesis: verum
end;
theorem Th32: :: WAYBEL_9:32
for T being non empty TopSpace
for N being net of T
for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M
proof
let T be non empty TopSpace; ::_thesis: for N being net of T
for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M
let N be net of T; ::_thesis: for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M
let x be Point of T; ::_thesis: ( x is_a_cluster_point_of N implies ex M being subnet of N st x in Lim M )
assume A1: x is_a_cluster_point_of N ; ::_thesis: ex M being subnet of N st x in Lim M
set q = the Element of N;
set S9 = { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } ;
reconsider O = [#] T as Element of (OpenNeighborhoods x) by YELLOW_6:30;
N . the Element of N in [#] T ;
then [ the Element of N,O] in { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } ;
then reconsider S9 = { [s,O] where s is Element of N, O is Element of (OpenNeighborhoods x) : N . s in O } as non empty set ;
set n = the mapping of N;
defpred S1[ set , set ] means ex s1, s2 being Element of N st
( s1 = $1 `1 & s2 = $2 `1 & s1 <= s2 & $2 `2 c= $1 `2 );
consider L being non empty strict RelStr such that
A2: the carrier of L = S9 and
A3: for a, b being Element of L holds
( a <= b iff S1[a,b] ) from YELLOW_0:sch_1();
deffunc H1( Element of L) -> set = the mapping of N . ($1 `1);
A4: for a being Element of L holds H1(a) in the carrier of T
proof
let a be Element of L; ::_thesis: H1(a) in the carrier of T
a in S9 by A2;
then consider s being Element of N, O being Element of (OpenNeighborhoods x) such that
A5: a = [s,O] and
N . s in O ;
the mapping of N . (a `1) = the mapping of N . s by A5, MCART_1:7;
hence H1(a) in the carrier of T ; ::_thesis: verum
end;
consider g being Function of the carrier of L, the carrier of T such that
A6: for x being Element of L holds g . x = H1(x) from FUNCT_2:sch_8(A4);
set M = NetStr(# the carrier of L, the InternalRel of L,g #);
for a, b being Element of NetStr(# the carrier of L, the InternalRel of L,g #) ex z being Element of NetStr(# the carrier of L, the InternalRel of L,g #) st
( a <= z & b <= z )
proof
let a, b be Element of NetStr(# the carrier of L, the InternalRel of L,g #); ::_thesis: ex z being Element of NetStr(# the carrier of L, the InternalRel of L,g #) st
( a <= z & b <= z )
a in S9 by A2;
then consider aa being Element of N, Oa being Element of (OpenNeighborhoods x) such that
A7: a = [aa,Oa] and
N . aa in Oa ;
b in S9 by A2;
then consider bb being Element of N, Ob being Element of (OpenNeighborhoods x) such that
A8: b = [bb,Ob] and
N . bb in Ob ;
consider z1 being Element of N such that
A9: aa <= z1 and
A10: bb <= z1 by YELLOW_6:def_3;
( Oa is a_neighborhood of x & Ob is a_neighborhood of x ) by Th21;
then Oa /\ Ob is a_neighborhood of x by CONNSP_2:2;
then N is_often_in Oa /\ Ob by A1, Def9;
then consider d being Element of N such that
A11: z1 <= d and
A12: N . d in Oa /\ Ob by WAYBEL_0:def_12;
Oa /\ Ob is Element of (OpenNeighborhoods x) by Th22;
then [d,(Oa /\ Ob)] in S9 by A12;
then reconsider z = [d,(Oa /\ Ob)] as Element of NetStr(# the carrier of L, the InternalRel of L,g #) by A2;
reconsider A1 = a, C7 = b, z2 = z as Element of L ;
A13: ( C7 `1 = bb & C7 `2 = Ob ) by A8, MCART_1:7;
take z ; ::_thesis: ( a <= z & b <= z )
A14: ( A1 `1 = aa & A1 `2 = Oa ) by A7, MCART_1:7;
A15: ( z2 `1 = d & z2 `2 = Oa /\ Ob ) by MCART_1:7;
( Oa /\ Ob c= Ob & bb <= d ) by A10, A11, XBOOLE_1:17, YELLOW_0:def_2;
then A16: C7 <= z2 by A3, A13, A15;
( Oa /\ Ob c= Oa & aa <= d ) by A9, A11, XBOOLE_1:17, YELLOW_0:def_2;
then A1 <= z2 by A3, A14, A15;
hence ( a <= z & b <= z ) by A16, YELLOW_0:1; ::_thesis: verum
end;
then reconsider M = NetStr(# the carrier of L, the InternalRel of L,g #) as prenet of T by YELLOW_6:def_3;
M is transitive
proof
let x, y, z be Element of M; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A17: x <= y and
A18: y <= z ; ::_thesis: x <= z
reconsider x1 = x, y1 = y, z1 = z as Element of L ;
x1 <= y1 by A17, YELLOW_0:1;
then consider sx, sy being Element of N such that
A19: sx = x1 `1 and
A20: ( sy = y1 `1 & sx <= sy & y1 `2 c= x1 `2 ) by A3;
y1 <= z1 by A18, YELLOW_0:1;
then consider s1, s2 being Element of N such that
A21: s1 = y1 `1 and
A22: s2 = z1 `1 and
A23: ( s1 <= s2 & z1 `2 c= y1 `2 ) by A3;
( sx <= s2 & z1 `2 c= x1 `2 ) by A20, A21, A23, XBOOLE_1:1, YELLOW_0:def_2;
then x1 <= z1 by A3, A19, A22;
hence x <= z by YELLOW_0:1; ::_thesis: verum
end;
then reconsider M = M as net of T ;
M is subnet of N
proof
deffunc H2( Element of L) -> set = $1 `1 ;
A24: for a being Element of L holds H2(a) in the carrier of N
proof
let a be Element of L; ::_thesis: H2(a) in the carrier of N
a in S9 by A2;
then consider s being Element of N, O being Element of (OpenNeighborhoods x) such that
A25: a = [s,O] and
N . s in O ;
a `1 = s by A25, MCART_1:7;
hence H2(a) in the carrier of N ; ::_thesis: verum
end;
consider f being Function of the carrier of L, the carrier of N such that
A26: for x being Element of L holds f . x = H2(x) from FUNCT_2:sch_8(A24);
reconsider f = f as Function of M,N ;
take f ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of M = the mapping of N * f & ( for b1 being Element of the carrier of N ex b2 being Element of the carrier of M st
for b3 being Element of the carrier of M holds
( not b2 <= b3 or b1 <= f . b3 ) ) )
for x being set st x in the carrier of M holds
g . x = ( the mapping of N * f) . x
proof
let x be set ; ::_thesis: ( x in the carrier of M implies g . x = ( the mapping of N * f) . x )
assume A27: x in the carrier of M ; ::_thesis: g . x = ( the mapping of N * f) . x
hence g . x = the mapping of N . (x `1) by A6
.= the mapping of N . (f . x) by A26, A27
.= ( the mapping of N * f) . x by A27, FUNCT_2:15 ;
::_thesis: verum
end;
hence the mapping of M = the mapping of N * f by FUNCT_2:12; ::_thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of M st
for b3 being Element of the carrier of M holds
( not b2 <= b3 or b1 <= f . b3 )
let m be Element of N; ::_thesis: ex b1 being Element of the carrier of M st
for b2 being Element of the carrier of M holds
( not b1 <= b2 or m <= f . b2 )
N . m in [#] T ;
then [m,O] in S9 ;
then reconsider n = [m,O] as Element of M by A2;
take n ; ::_thesis: for b1 being Element of the carrier of M holds
( not n <= b1 or m <= f . b1 )
let p be Element of M; ::_thesis: ( not n <= p or m <= f . p )
assume A28: n <= p ; ::_thesis: m <= f . p
reconsider n1 = n, p1 = p as Element of L ;
n1 <= p1 by A28, YELLOW_0:1;
then A29: ex s1, s2 being Element of N st
( s1 = n1 `1 & s2 = p1 `1 & s1 <= s2 & p1 `2 c= n1 `2 ) by A3;
f . p = p `1 by A26;
hence m <= f . p by A29, MCART_1:7; ::_thesis: verum
end;
then reconsider M = M as subnet of N ;
take M ; ::_thesis: x in Lim M
for V being a_neighborhood of x holds M is_eventually_in V
proof
set i = the Element of N;
let V be a_neighborhood of x; ::_thesis: M is_eventually_in V
( x in Int V & Int V is open ) by CONNSP_2:def_1;
then A30: Int V in the carrier of (OpenNeighborhoods x) by YELLOW_6:30;
then Int V is a_neighborhood of x by Th21;
then N is_often_in Int V by A1, Def9;
then consider s being Element of N such that
the Element of N <= s and
A31: N . s in Int V by WAYBEL_0:def_12;
A32: M is_eventually_in Int V
proof
[s,(Int V)] in S9 by A30, A31;
then reconsider j = [s,(Int V)] as Element of M by A2;
take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of M holds
( not j <= b1 or M . b1 in Int V )
let s9 be Element of M; ::_thesis: ( not j <= s9 or M . s9 in Int V )
assume A33: j <= s9 ; ::_thesis: M . s9 in Int V
reconsider j1 = j, s1 = s9 as Element of L ;
j1 <= s1 by A33, YELLOW_0:1;
then A34: ex s1, s2 being Element of N st
( s1 = j `1 & s2 = s9 `1 & s1 <= s2 & s9 `2 c= j `2 ) by A3;
s9 in S9 by A2;
then consider ss being Element of N, OO being Element of (OpenNeighborhoods x) such that
A35: s9 = [ss,OO] and
A36: N . ss in OO ;
A37: ( j `2 = Int V & s9 `2 = OO ) by A35, MCART_1:7;
M . s9 = the mapping of N . (s9 `1) by A6
.= N . ss by A35, MCART_1:7 ;
hence M . s9 in Int V by A36, A34, A37; ::_thesis: verum
end;
Int V c= V by TOPS_1:16;
hence M is_eventually_in V by A32, WAYBEL_0:8; ::_thesis: verum
end;
hence x in Lim M by YELLOW_6:def_15; ::_thesis: verum
end;
theorem Th33: :: WAYBEL_9:33
for L being non empty Hausdorff compact TopSpace
for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) holds
for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N
proof
let L be non empty Hausdorff compact TopSpace; ::_thesis: for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) holds
for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N
let N be net of L; ::_thesis: ( ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) implies for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N )
assume A1: for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ; ::_thesis: for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N
let c be Point of L; ::_thesis: ( c is_a_cluster_point_of N implies c in Lim N )
assume A2: c is_a_cluster_point_of N ; ::_thesis: c in Lim N
assume not c in Lim N ; ::_thesis: contradiction
then consider M being subnet of N such that
A3: for P being subnet of M holds not c in Lim P by YELLOW_6:37;
consider d being Point of L such that
A4: d is_a_cluster_point_of M by Th30;
A5: d is_a_cluster_point_of N by A4, Th31;
c <> d by A3, A4, Th32;
hence contradiction by A1, A2, A5; ::_thesis: verum
end;
theorem Th34: :: WAYBEL_9:34
for S being non empty TopSpace
for c being Point of S
for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
proof
let S be non empty TopSpace; ::_thesis: for c being Point of S
for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
let c be Point of S; ::_thesis: for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
let N be net of S; ::_thesis: for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
let A be Subset of S; ::_thesis: ( c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A implies c in A )
assume that
A1: c is_a_cluster_point_of N and
A2: A is closed and
A3: rng the mapping of N c= A ; ::_thesis: c in A
consider M being subnet of N such that
A4: c in Lim M by A1, Th32;
reconsider R = rng the mapping of M as Subset of S ;
ex f being Function of M,N st
( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) ) by YELLOW_6:def_9;
then R c= rng the mapping of N by RELAT_1:26;
then R c= A by A3, XBOOLE_1:1;
then A5: Cl R c= Cl A by PRE_TOPC:19;
c in Cl R by A4, Th24;
then c in Cl A by A5;
hence c in A by A2, PRE_TOPC:22; ::_thesis: verum
end;
Lm5: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
proof
let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
let N be net of S; ::_thesis: for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N implies d is_>=_than rng the mapping of N )
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: N is eventually-directed and
A4: c is_a_cluster_point_of N ; ::_thesis: d is_>=_than rng the mapping of N
let i be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not i in rng the mapping of N or i <= d )
assume i in rng the mapping of N ; ::_thesis: i <= d
then consider iJ being set such that
A5: iJ in dom the mapping of N and
A6: the mapping of N . iJ = i by FUNCT_1:def_3;
reconsider i1 = iJ as Element of N by A5;
uparrow (N . i1) is closed by A2, Th27;
then A7: Cl (uparrow (N . i1)) = uparrow (N . i1) by PRE_TOPC:22;
N is_eventually_in uparrow (N . i1)
proof
consider j being Element of N such that
A8: for k being Element of N st j <= k holds
N . i1 <= N . k by A3, WAYBEL_0:11;
take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in uparrow (N . i1) )
let k be Element of N; ::_thesis: ( not j <= k or N . k in uparrow (N . i1) )
assume j <= k ; ::_thesis: N . k in uparrow (N . i1)
then N . i1 <= N . k by A8;
hence N . k in uparrow (N . i1) by WAYBEL_0:18; ::_thesis: verum
end;
then consider t being Element of N such that
A9: for j being Element of N st t <= j holds
N . j in uparrow (N . i1) by WAYBEL_0:def_11;
reconsider A = N | t as subnet of N ;
A10: rng the mapping of A c= uparrow (N . i1)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng the mapping of A or q in uparrow (N . i1) )
assume q in rng the mapping of A ; ::_thesis: q in uparrow (N . i1)
then consider x being set such that
A11: x in dom the mapping of A and
A12: q = the mapping of A . x by FUNCT_1:def_3;
reconsider x = x as Element of A by A11;
consider y being Element of N such that
A13: y = x and
A14: t <= y by Def7;
A . x = N . y by A13, Th16;
hence q in uparrow (N . i1) by A9, A12, A14; ::_thesis: verum
end;
c is_a_cluster_point_of A
proof
let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: A is_often_in O
let i be Element of A; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of A st
( i <= b1 & A . b1 in O )
consider i2 being Element of N such that
A15: i2 = i and
A16: t <= i2 by Def7;
N is_often_in O by A4, Def9;
then consider j2 being Element of N such that
A17: i2 <= j2 and
A18: N . j2 in O by WAYBEL_0:def_12;
t <= j2 by A16, A17, YELLOW_0:def_2;
then reconsider j = j2 as Element of A by Def7;
take j ; ::_thesis: ( i <= j & A . j in O )
A is full SubNetStr of N by Th14;
hence i <= j by A15, A17, YELLOW_6:12; ::_thesis: A . j in O
thus A . j in O by A18, Th16; ::_thesis: verum
end;
then consider M being subnet of A such that
A19: c in Lim M by Th32;
reconsider R = rng the mapping of M as Subset of S ;
A20: uparrow (N . i1) = { z where z is Element of S : z "/\" (N . i1) = N . i1 } by Lm1;
ex f being Function of M,A st
( the mapping of M = the mapping of A * f & ( for m being Element of A ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) ) by YELLOW_6:def_9;
then R c= rng the mapping of A by RELAT_1:26;
then R c= uparrow (N . i1) by A10, XBOOLE_1:1;
then A21: Cl R c= Cl (uparrow (N . i1)) by PRE_TOPC:19;
c in Cl R by A19, Th24;
then c in uparrow (N . i1) by A7, A21;
then ex z being Element of S st
( c = z & z "/\" (N . i1) = N . i1 ) by A20;
hence i <= d by A1, A6, YELLOW_0:25; ::_thesis: verum
end;
Lm6: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
proof
let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let N be net of S; ::_thesis: for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N implies for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b )
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: c is_a_cluster_point_of N ; ::_thesis: for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
let b be Element of S; ::_thesis: ( rng the mapping of N is_<=_than b implies d <= b )
assume A4: rng the mapping of N is_<=_than b ; ::_thesis: d <= b
A5: now__::_thesis:_for_i_being_Element_of_N_holds_N_._i_in_{b}_"/\"_([#]_S)
let i be Element of N; ::_thesis: N . i in {b} "/\" ([#] S)
A6: the carrier of N = dom the mapping of N by FUNCT_2:def_1;
N . i in rng the mapping of N by A6, FUNCT_1:def_3;
then N . i <= b by A4, LATTICE3:def_9;
then A7: b "/\" (N . i) = N . i by YELLOW_0:25;
b in {b} by TARSKI:def_1;
hence N . i in {b} "/\" ([#] S) by A7, YELLOW_4:37; ::_thesis: verum
end;
A8: rng the mapping of N c= {b} "/\" ([#] S)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of N or y in {b} "/\" ([#] S) )
assume y in rng the mapping of N ; ::_thesis: y in {b} "/\" ([#] S)
then consider x being set such that
A9: x in dom the mapping of N and
A10: y = the mapping of N . x by FUNCT_1:def_3;
reconsider x = x as Element of N by A9;
y = N . x by A10;
hence y in {b} "/\" ([#] S) by A5; ::_thesis: verum
end;
downarrow b is closed by A2, Th28;
then {b} "/\" ([#] S) is closed by Th5;
then ( {b} "/\" ([#] S) = { (b "/\" y) where y is Element of S : y in [#] S } & c in {b} "/\" ([#] S) ) by A3, A8, Th34, YELLOW_4:42;
then ex y being Element of S st
( c = b "/\" y & y in [#] S ) ;
hence d <= b by A1, YELLOW_0:23; ::_thesis: verum
end;
theorem Th35: :: WAYBEL_9:35
for S being Hausdorff compact TopLattice
for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N
proof
let S be Hausdorff compact TopLattice; ::_thesis: for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N
let c be Point of S; ::_thesis: for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N
let N be net of S; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N implies c = sup N )
assume A1: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N ) ; ::_thesis: c = sup N
reconsider c9 = c as Element of S ;
( c9 is_>=_than rng the mapping of N & ( for b being Element of S st rng the mapping of N is_<=_than b holds
c9 <= b ) ) by A1, Lm5, Lm6;
hence c = sup (rng the mapping of N) by YELLOW_0:30
.= sup N by YELLOW_2:def_5 ;
::_thesis: verum
end;
Lm7: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
proof
let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
let N be net of S; ::_thesis: for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N implies d is_<=_than rng the mapping of N )
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: N is eventually-filtered and
A4: c is_a_cluster_point_of N ; ::_thesis: d is_<=_than rng the mapping of N
let i be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not i in rng the mapping of N or d <= i )
assume i in rng the mapping of N ; ::_thesis: d <= i
then consider iJ being set such that
A5: iJ in dom the mapping of N and
A6: the mapping of N . iJ = i by FUNCT_1:def_3;
reconsider i1 = iJ as Element of N by A5;
downarrow (N . i1) is closed by A2, Th28;
then A7: Cl (downarrow (N . i1)) = downarrow (N . i1) by PRE_TOPC:22;
N is_eventually_in downarrow (N . i1)
proof
consider j being Element of N such that
A8: for k being Element of N st j <= k holds
N . i1 >= N . k by A3, WAYBEL_0:12;
take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in downarrow (N . i1) )
let k be Element of N; ::_thesis: ( not j <= k or N . k in downarrow (N . i1) )
assume j <= k ; ::_thesis: N . k in downarrow (N . i1)
then N . i1 >= N . k by A8;
hence N . k in downarrow (N . i1) by WAYBEL_0:17; ::_thesis: verum
end;
then consider t being Element of N such that
A9: for j being Element of N st t <= j holds
N . j in downarrow (N . i1) by WAYBEL_0:def_11;
reconsider A = N | t as subnet of N ;
A10: rng the mapping of A c= downarrow (N . i1)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng the mapping of A or q in downarrow (N . i1) )
assume q in rng the mapping of A ; ::_thesis: q in downarrow (N . i1)
then consider x being set such that
A11: x in dom the mapping of A and
A12: q = the mapping of A . x by FUNCT_1:def_3;
reconsider x = x as Element of A by A11;
consider y being Element of N such that
A13: y = x and
A14: t <= y by Def7;
A . x = N . y by A13, Th16;
hence q in downarrow (N . i1) by A9, A12, A14; ::_thesis: verum
end;
c is_a_cluster_point_of A
proof
let O be a_neighborhood of c; :: according to WAYBEL_9:def_9 ::_thesis: A is_often_in O
let i be Element of A; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of A st
( i <= b1 & A . b1 in O )
consider i2 being Element of N such that
A15: i2 = i and
A16: t <= i2 by Def7;
N is_often_in O by A4, Def9;
then consider j2 being Element of N such that
A17: i2 <= j2 and
A18: N . j2 in O by WAYBEL_0:def_12;
t <= j2 by A16, A17, YELLOW_0:def_2;
then reconsider j = j2 as Element of A by Def7;
take j ; ::_thesis: ( i <= j & A . j in O )
A is full SubNetStr of N by Th14;
hence i <= j by A15, A17, YELLOW_6:12; ::_thesis: A . j in O
thus A . j in O by A18, Th16; ::_thesis: verum
end;
then consider M being subnet of A such that
A19: c in Lim M by Th32;
reconsider R = rng the mapping of M as Subset of S ;
A20: downarrow (N . i1) = { z where z is Element of S : z "\/" (N . i1) = N . i1 } by Lm2;
ex f being Function of M,A st
( the mapping of M = the mapping of A * f & ( for m being Element of A ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) ) by YELLOW_6:def_9;
then R c= rng the mapping of A by RELAT_1:26;
then R c= downarrow (N . i1) by A10, XBOOLE_1:1;
then A21: Cl R c= Cl (downarrow (N . i1)) by PRE_TOPC:19;
c in Cl R by A19, Th24;
then c in downarrow (N . i1) by A7, A21;
then ex z being Element of S st
( c = z & z "\/" (N . i1) = N . i1 ) by A20;
hence d <= i by A1, A6, YELLOW_0:24; ::_thesis: verum
end;
Lm8: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
proof
let S be Hausdorff compact TopLattice; ::_thesis: for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
let N be net of S; ::_thesis: for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
let c be Point of S; ::_thesis: for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
let d be Element of S; ::_thesis: ( c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N implies for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b )
assume that
A1: c = d and
A2: for x being Element of S holds x "/\" is continuous and
A3: c is_a_cluster_point_of N ; ::_thesis: for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
let b be Element of S; ::_thesis: ( rng the mapping of N is_>=_than b implies d >= b )
assume A4: rng the mapping of N is_>=_than b ; ::_thesis: d >= b
A5: now__::_thesis:_for_i_being_Element_of_N_holds_N_._i_in_{b}_"\/"_([#]_S)
let i be Element of N; ::_thesis: N . i in {b} "\/" ([#] S)
A6: the carrier of N = dom the mapping of N by FUNCT_2:def_1;
N . i in rng the mapping of N by A6, FUNCT_1:def_3;
then N . i >= b by A4, LATTICE3:def_8;
then A7: b "\/" (N . i) = N . i by YELLOW_0:24;
b in {b} by TARSKI:def_1;
hence N . i in {b} "\/" ([#] S) by A7, YELLOW_4:10; ::_thesis: verum
end;
A8: rng the mapping of N c= {b} "\/" ([#] S)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of N or y in {b} "\/" ([#] S) )
assume y in rng the mapping of N ; ::_thesis: y in {b} "\/" ([#] S)
then consider x being set such that
A9: x in dom the mapping of N and
A10: y = the mapping of N . x by FUNCT_1:def_3;
reconsider x = x as Element of N by A9;
y = N . x by A10;
hence y in {b} "\/" ([#] S) by A5; ::_thesis: verum
end;
uparrow b is closed by A2, Th27;
then {b} "\/" ([#] S) is closed by Th4;
then ( {b} "\/" ([#] S) = { (b "\/" y) where y is Element of S : y in [#] S } & c in {b} "\/" ([#] S) ) by A3, A8, Th34, YELLOW_4:15;
then ex y being Element of S st
( c = b "\/" y & y in [#] S ) ;
hence d >= b by A1, YELLOW_0:22; ::_thesis: verum
end;
theorem Th36: :: WAYBEL_9:36
for S being Hausdorff compact TopLattice
for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N
proof
let S be Hausdorff compact TopLattice; ::_thesis: for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N
let c be Point of S; ::_thesis: for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N
let N be net of S; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N implies c = inf N )
assume A1: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N ) ; ::_thesis: c = inf N
reconsider c9 = c as Element of S ;
( c9 is_<=_than rng the mapping of N & ( for b being Element of S st rng the mapping of N is_>=_than b holds
c9 >= b ) ) by A1, Lm7, Lm8;
hence c = inf (rng the mapping of N) by YELLOW_0:31
.= inf N by YELLOW_2:def_6 ;
::_thesis: verum
end;
begin
theorem Th37: :: WAYBEL_9:37
for S being Hausdorff TopLattice st ( for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) holds
S is meet-continuous
proof
let S be Hausdorff TopLattice; ::_thesis: ( ( for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous )
assume that
A1: for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) and
A2: for x being Element of S holds x "/\" is continuous ; ::_thesis: S is meet-continuous
for X being non empty directed Subset of S holds ex_sup_of X,S
proof
let X be non empty directed Subset of S; ::_thesis: ex_sup_of X,S
reconsider n = id X as Function of X, the carrier of S by FUNCT_2:7;
set N = NetStr(# X,( the InternalRel of S |_2 X),n #);
NetStr(# X,( the InternalRel of S |_2 X),n #) is eventually-directed by WAYBEL_2:20;
then A3: ex_sup_of NetStr(# X,( the InternalRel of S |_2 X),n #) by A1;
rng the mapping of NetStr(# X,( the InternalRel of S |_2 X),n #) = X by RELAT_1:45;
hence ex_sup_of X,S by A3, Def3; ::_thesis: verum
end;
hence S is up-complete by WAYBEL_0:75; :: according to WAYBEL_2:def_7 ::_thesis: S is satisfying_MC
for x being Element of S
for M being net of S st M is eventually-directed holds
x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S))))
proof
let x be Element of S; ::_thesis: for M being net of S st M is eventually-directed holds
x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S))))
let M be net of S; ::_thesis: ( M is eventually-directed implies x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S)))) )
assume A4: M is eventually-directed ; ::_thesis: x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S))))
A5: sup M in Lim M by A1, A4;
then reconsider M1 = M as convergent net of S by YELLOW_6:def_16;
set xM = x "/\" M;
x "/\" M is eventually-directed by A4, WAYBEL_2:27;
then A6: sup (x "/\" M) in Lim (x "/\" M) by A1;
x "/\" is continuous by A2;
then A7: x "/\" (lim M1) in Lim (x "/\" M1) by Th26;
reconsider xM = x "/\" M as convergent net of S by A6, YELLOW_6:def_16;
thus x "/\" (sup M) = x "/\" (lim M1) by A5, YELLOW_6:def_17
.= lim xM by A7, YELLOW_6:def_17
.= Sup by A6, YELLOW_6:def_17
.= sup (rng the mapping of xM) by YELLOW_2:def_5
.= sup ({x} "/\" (rng (netmap (M,S)))) by WAYBEL_2:23 ; ::_thesis: verum
end;
hence S is satisfying_MC by Th9; ::_thesis: verum
end;
theorem Th38: :: WAYBEL_9:38
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N )
proof
let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) )
assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N )
let N be net of S; ::_thesis: ( N is eventually-directed implies ( ex_sup_of N & sup N in Lim N ) )
assume A2: N is eventually-directed ; ::_thesis: ( ex_sup_of N & sup N in Lim N )
A3: for c, d being Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d
proof
let c, d be Point of S; ::_thesis: ( c is_a_cluster_point_of N & d is_a_cluster_point_of N implies c = d )
assume that
A4: c is_a_cluster_point_of N and
A5: d is_a_cluster_point_of N ; ::_thesis: c = d
thus c = sup N by A1, A2, A4, Th35
.= d by A1, A2, A5, Th35 ; ::_thesis: verum
end;
consider c being Point of S such that
A6: c is_a_cluster_point_of N by Th30;
thus ex_sup_of N ::_thesis: sup N in Lim N
proof
reconsider d = c as Element of S ;
set X = rng the mapping of N;
( rng the mapping of N is_<=_than d & ( for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b ) ) by A1, A2, A6, Lm5, Lm6;
hence ex_sup_of rng the mapping of N,S by YELLOW_0:15; :: according to WAYBEL_9:def_3 ::_thesis: verum
end;
c = sup N by A1, A2, A6, Th35;
hence sup N in Lim N by A6, A3, Th33; ::_thesis: verum
end;
theorem Th39: :: WAYBEL_9:39
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N )
proof
let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N ) )
assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N )
let N be net of S; ::_thesis: ( N is eventually-filtered implies ( ex_inf_of N & inf N in Lim N ) )
assume A2: N is eventually-filtered ; ::_thesis: ( ex_inf_of N & inf N in Lim N )
A3: for c, d being Point of S st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d
proof
let c, d be Point of S; ::_thesis: ( c is_a_cluster_point_of N & d is_a_cluster_point_of N implies c = d )
assume that
A4: c is_a_cluster_point_of N and
A5: d is_a_cluster_point_of N ; ::_thesis: c = d
thus c = inf N by A1, A2, A4, Th36
.= d by A1, A2, A5, Th36 ; ::_thesis: verum
end;
consider c being Point of S such that
A6: c is_a_cluster_point_of N by Th30;
thus ex_inf_of N ::_thesis: inf N in Lim N
proof
reconsider d = c as Element of S ;
set X = rng the mapping of N;
( rng the mapping of N is_>=_than d & ( for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b ) ) by A1, A2, A6, Lm7, Lm8;
hence ex_inf_of rng the mapping of N,S by YELLOW_0:16; :: according to WAYBEL_9:def_4 ::_thesis: verum
end;
c = inf N by A1, A2, A6, Th36;
hence inf N in Lim N by A6, A3, Th33; ::_thesis: verum
end;
theorem :: WAYBEL_9:40
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
S is bounded
proof
let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies S is bounded )
assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: S is bounded
thus S is lower-bounded :: according to YELLOW_0:def_6 ::_thesis: S is upper-bounded
proof
reconsider x = inf (S opp+id) as Element of S ;
take x ; :: according to YELLOW_0:def_4 ::_thesis: x is_<=_than the carrier of S
A2: rng the mapping of (S opp+id) = rng (id S) by Def6
.= the carrier of S by RELAT_1:45 ;
then A3: x = "/\" ( the carrier of S,S) by YELLOW_2:def_6;
ex_inf_of S opp+id by A1, Th39;
then ex_inf_of the carrier of S,S by A2, Def4;
hence x is_<=_than the carrier of S by A3, YELLOW_0:31; ::_thesis: verum
end;
reconsider x = sup (S +id) as Element of S ;
take x ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of S is_<=_than x
A4: rng the mapping of (S +id) = rng (id S) by Def5
.= the carrier of S by RELAT_1:45 ;
then A5: x = "\/" ( the carrier of S,S) by YELLOW_2:def_5;
ex_sup_of S +id by A1, Th38;
then ex_sup_of the carrier of S,S by A4, Def3;
hence the carrier of S is_<=_than x by A5, YELLOW_0:30; ::_thesis: verum
end;
theorem :: WAYBEL_9:41
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
S is meet-continuous
proof
let S be Hausdorff compact TopLattice; ::_thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous )
assume A1: for x being Element of S holds x "/\" is continuous ; ::_thesis: S is meet-continuous
then for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) by Th38;
hence S is meet-continuous by A1, Th37; ::_thesis: verum
end;