begin
begin
theorem Th30:
theorem Th32:
theorem Th33:
theorem
Lm1:
for T being non empty TopSpace
for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
begin
theorem Th45:
theorem
begin
:: deftheorem Def11 defines Lim_inf KURATO_2:def 1 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b3 being Subset of T holds
( b3 = Lim_inf S iff for p being Point of T holds
( p in b3 iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) );
theorem Th48:
theorem Th49:
theorem
theorem Th52:
theorem
theorem
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem
theorem Th62:
theorem
theorem
begin
:: deftheorem Def12 defines Lim_sup KURATO_2:def 2 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b3 being Subset of T holds
( b3 = Lim_sup S iff for x being set holds
( x in b3 iff ex A being subsequence of S st x in Lim_inf A ) );
theorem
theorem Th66:
theorem Th67:
theorem
theorem Th69:
theorem
theorem
theorem Th72:
theorem
theorem Th74:
theorem
theorem