begin
theorem Th1:
Lm1:
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
Lm2:
for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
theorem Th2:
theorem
theorem Th4:
theorem
theorem Th6:
theorem
theorem Th8:
begin
:: deftheorem Def1 defines dense TEX_3:def 1 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is dense iff for A being Subset of X st A = the carrier of IT holds
A is dense );
theorem Th9:
theorem Th10:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def2 defines everywhere_dense TEX_3:def 2 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense );
theorem Th16:
theorem Th17:
theorem
theorem
theorem
theorem
theorem
theorem Th23:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def3 defines boundary TEX_3:def 3 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is boundary iff for A being Subset of X st A = the carrier of IT holds
A is boundary );
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem Th34:
:: deftheorem Def4 defines nowhere_dense TEX_3:def 4 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense );
theorem Th35:
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th62:
theorem
theorem
theorem
theorem
theorem Th67:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem