begin
:: deftheorem Def1 defines antitone WAYBEL_9:def 1 :
theorem Th1:
theorem Th2:
theorem
Lm1:
for L being reflexive antisymmetric with_infima RelStr
for x being Element of holds uparrow x = { z where z is Element of : z "/\" x = x }
theorem Th4:
Lm2:
for L being reflexive antisymmetric with_suprema RelStr
for x being Element of holds downarrow x = { z where z is Element of : z "\/" x = x }
theorem Th5:
theorem
theorem Th7:
theorem Th8:
Lm3:
for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of
for n being Function of D,the carrier of L holds NetStr(# D,(the InternalRel of L |_2 D),n #) is net of
theorem Th9:
theorem Th10:
begin
:: deftheorem defines inf WAYBEL_9:def 2 :
:: deftheorem Def3 defines ex_sup_of WAYBEL_9:def 3 :
:: deftheorem Def4 defines ex_inf_of WAYBEL_9:def 4 :
:: deftheorem Def5 defines +id WAYBEL_9:def 5 :
:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :
theorem Th11:
:: deftheorem Def7 defines | WAYBEL_9:def 7 :
theorem
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
definition
let S be non
empty 1-sorted ;
let T be
1-sorted ;
let f be
Function of
S,
T;
let N be
NetStr of
S;
func f * N -> strict NetStr of
T means :
Def8:
(
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 of 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 )
uniqueness
for b1, b2 being strict NetStr of 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 :
theorem Th18:
begin
theorem
theorem
Lm4:
for tau being Subset-Family of
for r being Relation of st tau = {{} ,{0 }} & r = {[0 ,0 ]} holds
( TopRelStr(# {0 },r,tau #) is trivial & TopRelStr(# {0 },r,tau #) is reflexive & not TopRelStr(# {0 },r,tau #) is empty & TopRelStr(# {0 },r,tau #) is discrete & TopRelStr(# {0 },r,tau #) is finite )
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def 9 :
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
Lm5:
for S being Hausdorff compact TopLattice
for N being net of
for c being Point of
for d being Element of st c = d & ( for x being Element of holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
Lm6:
for S being Hausdorff compact TopLattice
for N being net of
for c being Point of
for d being Element of st c = d & ( for x being Element of holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of st rng the mapping of N is_<=_than b holds
d <= b
theorem Th35:
Lm7:
for S being Hausdorff compact TopLattice
for N being net of
for c being Point of
for d being Element of st c = d & ( for x being Element of holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
Lm8:
for S being Hausdorff compact TopLattice
for N being net of
for c being Point of
for d being Element of st c = d & ( for x being Element of holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of st rng the mapping of N is_>=_than b holds
d >= b
theorem Th36:
begin
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem