:: On the characterizations of compactness
:: by Grzegorz Bancerek , Noboru Endou and Yuji Sakai
::
:: Received July 29, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: YELLOW19:1
canceled;
theorem Th2: :: YELLOW19:2
:: deftheorem defines NeighborhoodSystem YELLOW19:def 1 :
theorem Th3: :: YELLOW19:3
theorem Th4: :: YELLOW19:4
theorem :: YELLOW19:5
theorem :: YELLOW19:6
:: deftheorem Def2 defines Subset YELLOW19:def 2 :
theorem :: YELLOW19:7
theorem Th8: :: YELLOW19:8
theorem Th9: :: YELLOW19:9
theorem :: YELLOW19:10
:: deftheorem defines a_filter YELLOW19:def 3 :
theorem Th11: :: YELLOW19:11
theorem Th12: :: YELLOW19:12
theorem Th13: :: YELLOW19:13
definition
let L be non
empty 1-sorted ;
let O be non
empty Subset of
L;
let F be
Filter of
(BoolePoset O);
func a_net F -> non
empty strict NetStr of
L means :
Def4:
:: YELLOW19:def 4
( the
carrier of
it = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for
i,
j being
Element of
it holds
(
i <= j iff
j `2 c= i `2 ) ) & ( for
i being
Element of
it 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 L, f is Element of F : a in f } & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 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 L, f is Element of F : a in f } & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) & the carrier of b2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b2 holds b2 . i = i `1 ) holds
b1 = b2
end;
:: deftheorem Def4 defines a_net YELLOW19:def 4 :
theorem Th14: :: YELLOW19:14
theorem Th15: :: YELLOW19:15
theorem Th16: :: YELLOW19:16
theorem Th17: :: YELLOW19:17
theorem Th18: :: YELLOW19:18
theorem :: YELLOW19:19
canceled;
theorem Th20: :: YELLOW19:20
theorem Th21: :: YELLOW19:21
theorem Th22: :: YELLOW19:22
theorem Th23: :: YELLOW19:23
theorem Th24: :: YELLOW19:24
theorem :: YELLOW19:25
theorem :: YELLOW19:26
theorem Th27: :: YELLOW19:27
theorem Th28: :: YELLOW19:28
theorem :: YELLOW19:29
theorem :: YELLOW19:30
theorem Th31: :: YELLOW19:31
theorem :: YELLOW19:32
Lm1:
for T being non empty TopSpace st T is compact holds
for N being net of T ex x being Point of T st x is_a_cluster_point_of N
Lm2:
for T being non empty TopSpace st ( for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ) holds
T is compact
theorem Th33: :: YELLOW19:33
theorem :: YELLOW19:34
theorem Th35: :: YELLOW19:35
theorem :: YELLOW19:36
theorem :: YELLOW19:37
:: deftheorem defines Cauchy YELLOW19:def 5 :
theorem :: YELLOW19:38