begin
Lm1:
for T being empty TopSpace
for A being Subset of T holds A = {}
;
theorem Th1:
theorem
canceled;
theorem
begin
theorem
canceled;
theorem Th5:
:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :
for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Fr F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Fr B & B in F ) ) );
theorem
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem Th16:
begin
:: deftheorem Def2 defines is_an_accumulation_point_of TOPGEN_1:def 2 :
for T being TopStruct
for A being Subset of T
for x being set holds
( x is_an_accumulation_point_of A iff x in Cl (A \ {x}) );
theorem Th17:
:: deftheorem Def3 defines Der TOPGEN_1:def 3 :
for T being TopStruct
for A, b3 being Subset of T holds
( b3 = Der A iff for x being set st x in the carrier of T holds
( x in b3 iff x is_an_accumulation_point_of A ) );
theorem Th18:
theorem Th19:
theorem
theorem
begin
:: deftheorem Def4 defines is_isolated_in TOPGEN_1:def 4 :
for T being TopSpace
for A being Subset of T
for x being set holds
( x is_isolated_in A iff ( x in A & not x is_an_accumulation_point_of A ) );
theorem
theorem Th23:
theorem Th24:
:: deftheorem Def5 defines isolated TOPGEN_1:def 5 :
for T being TopSpace
for p being Point of T holds
( p is isolated iff p is_isolated_in [#] T );
theorem
begin
:: deftheorem Def6 defines Der TOPGEN_1:def 6 :
for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Der F iff for A being Subset of T holds
( A in b3 iff ex B being Subset of T st
( A = Der B & B in F ) ) );
theorem
theorem
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
begin
:: deftheorem Def7 defines dense-in-itself TOPGEN_1:def 7 :
for T being TopSpace
for A being Subset of T holds
( A is dense-in-itself iff A c= Der A );
:: deftheorem defines dense-in-itself TOPGEN_1:def 8 :
for T being non empty TopSpace holds
( T is dense-in-itself iff [#] T is dense-in-itself );
theorem Th38:
:: deftheorem Def9 defines dense-in-itself TOPGEN_1:def 9 :
for T being TopSpace
for F being Subset-Family of T holds
( F is dense-in-itself iff for A being Subset of T st A in F holds
A is dense-in-itself );
theorem Th39:
theorem Th40:
theorem
begin
:: deftheorem Def10 defines perfect TOPGEN_1:def 10 :
for T being TopSpace
for A being Subset of T holds
( A is perfect iff ( A is closed & A is dense-in-itself ) );
theorem Th42:
Lm2:
for T being TopSpace
for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A
theorem Th43:
theorem Th44:
begin
:: deftheorem Def11 defines scattered TOPGEN_1:def 11 :
for T being TopSpace
for A being Subset of T holds
( A is scattered iff for B being Subset of T holds
( B is empty or not B c= A or not B is dense-in-itself ) );
theorem Th45:
theorem
theorem Th47:
begin
:: deftheorem Def12 defines density TOPGEN_1:def 12 :
for T being TopSpace
for b2 being cardinal number holds
( b2 = density T iff ( ex A being Subset of T st
( A is dense & b2 = card A ) & ( for B being Subset of T st B is dense holds
b2 c= card B ) ) );
:: deftheorem Def13 defines separable TOPGEN_1:def 13 :
for T being TopSpace holds
( T is separable iff density T c= omega );
theorem
canceled;
theorem Th49:
begin
theorem
Lm3:
RAT = REAL \ IRRAT
theorem
theorem
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem