begin
theorem
canceled;
theorem Th2:
:: deftheorem defines NeighborhoodSystem YELLOW19:def 1 :
theorem Th3:
theorem Th4:
theorem
theorem
:: deftheorem Def2 defines Subset YELLOW19:def 2 :
theorem
theorem Th8:
theorem Th9:
theorem
:: deftheorem defines a_filter YELLOW19:def 3 :
theorem Th11:
theorem Th12:
theorem Th13:
definition
let L be non
empty 1-sorted ;
let O be non
empty Subset of ;
let F be
Filter of
BoolePoset O;
func a_net F -> non
empty strict NetStr of
L means :
Def4:
( the
carrier of
it = { [a,f] where a is Element of , f is Element of F : a in f } & ( for
i,
j being
Element of holds
(
i <= j iff
j `2 c= i `2 ) ) & ( for
i being
Element of holds
it . i = i `1 ) );
existence
ex b1 being non empty strict NetStr of L st
( the carrier of b1 = { [a,f] where a is Element of , f is Element of F : a in f } & ( for i, j being Element of holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of holds b1 . i = i `1 ) )
uniqueness
for b1, b2 being non empty strict NetStr of L st the carrier of b1 = { [a,f] where a is Element of , f is Element of F : a in f } & ( for i, j being Element of holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of holds b1 . i = i `1 ) & the carrier of b2 = { [a,f] where a is Element of , f is Element of F : a in f } & ( for i, j being Element of holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of holds b2 . i = i `1 ) holds
b1 = b2
end;
:: deftheorem Def4 defines a_net YELLOW19:def 4 :
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
canceled;
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem Th28:
theorem
theorem
theorem Th31:
theorem
Lm1:
for T being non empty TopSpace st T is compact holds
for N being net of ex x being Point of st x is_a_cluster_point_of N
Lm2:
for T being non empty TopSpace st ( for N being net of st N in NetUniv T holds
ex x being Point of st x is_a_cluster_point_of N ) holds
T is compact
theorem Th33:
theorem
theorem Th35:
theorem
theorem
:: deftheorem defines Cauchy YELLOW19:def 5 :
theorem