begin
:: deftheorem Def1 defines T_0 TSP_2:def 1 :
:: deftheorem Def2 defines T_0 TSP_2:def 2 :
:: deftheorem defines T_0 TSP_2:def 3 :
:: deftheorem Def4 defines maximal_T_0 TSP_2:def 4 :
theorem
:: deftheorem Def5 defines maximal_T_0 TSP_2:def 5 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
:: deftheorem Def6 defines maximal_T_0 TSP_2:def 6 :
theorem Th9:
theorem Th10:
begin
:: deftheorem Def7 defines maximal_T_0 TSP_2:def 7 :
theorem Th11:
:: deftheorem defines maximal_T_0 TSP_2:def 8 :
theorem Th12:
theorem
theorem Th14:
theorem
theorem Th16:
theorem
begin
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem
Lm2:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
Lm3:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
Lm4:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
Lm5:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
Lm6:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
:: deftheorem Def9 defines Stone-retraction TSP_2:def 9 :
theorem
theorem Th25:
theorem Th26:
:: deftheorem Def10 defines Stone-retraction TSP_2:def 10 :
:: deftheorem Def11 defines Stone-retraction TSP_2:def 11 :
theorem Th27:
theorem
:: deftheorem Def12 defines Stone-retraction TSP_2:def 12 :
theorem Th29:
theorem
theorem
theorem
theorem
theorem
theorem