:: Maximal Kolmogorov Subspaces of a Topological Space as StoneRetracts of the Ambient Space
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: 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 :: TSP_2:1
:: deftheorem Def5 defines maximal_T_0 TSP_2:def 5 :
theorem Th2: :: TSP_2:2
theorem Th3: :: TSP_2:3
theorem Th4: :: TSP_2:4
theorem Th5: :: TSP_2:5
theorem Th6: :: TSP_2:6
theorem :: TSP_2:7
theorem :: TSP_2:8
:: deftheorem Def6 defines maximal_T_0 TSP_2:def 6 :
theorem Th9: :: TSP_2:9
theorem Th10: :: TSP_2:10
:: deftheorem Def7 defines maximal_T_0 TSP_2:def 7 :
theorem Th11: :: TSP_2:11
:: deftheorem defines maximal_T_0 TSP_2:def 8 :
theorem Th12: :: TSP_2:12
theorem :: TSP_2:13
theorem Th14: :: TSP_2:14
theorem :: TSP_2:15
theorem Th16: :: TSP_2:16
theorem :: TSP_2:17
theorem Th18: :: TSP_2:18
theorem :: TSP_2:19
theorem Th20: :: TSP_2:20
theorem Th21: :: TSP_2:21
theorem Th22: :: TSP_2:22
theorem :: TSP_2:23
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 :: TSP_2:24
theorem Th25: :: TSP_2:25
theorem Th26: :: TSP_2:26
:: deftheorem Def10 defines Stone-retraction TSP_2:def 10 :
:: deftheorem Def11 defines Stone-retraction TSP_2:def 11 :
theorem Th27: :: TSP_2:27
theorem :: TSP_2:28
:: deftheorem Def12 defines Stone-retraction TSP_2:def 12 :
theorem Th29: :: TSP_2:29
theorem :: TSP_2:30
theorem :: TSP_2:31
theorem :: TSP_2:32
theorem :: TSP_2:33
theorem :: TSP_2:34
theorem :: TSP_2:35