:: $T_0$ Topological Spaces :: by Mariusz \.Zynel and Adam Guzowski :: :: Received May 6, 1994 :: Copyright (c) 1994-2012 Association of Mizar Users begin :: :: Preliminaries :: theorem Th1: :: T_0TOPSP:1 for X, Y being non empty set for f being Function of X,Y for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds x2 in A ) holds f " (f .: A) = A proofend; :: Homeomorphic TopSpaces definition let T, S be TopStruct ; predT,S are_homeomorphic means :: T_0TOPSP:def 1 ex f being Function of T,S st f is being_homeomorphism ; end; :: deftheorem defines are_homeomorphic T_0TOPSP:def_1_:_ for T, S being TopStruct holds ( T,S are_homeomorphic iff ex f being Function of T,S st f is being_homeomorphism ); :: Open Function definition let T, S be TopStruct ; let f be Function of T,S; attrf is open means :Def2: :: T_0TOPSP:def 2 for A being Subset of T st A is open holds f .: A is open ; correctness ; end; :: deftheorem Def2 defines open T_0TOPSP:def_2_:_ for T, S being TopStruct for f being Function of T,S holds ( f is open iff for A being Subset of T st A is open holds f .: A is open ); :: :: Indiscernibility Relation :: definition let T be non empty TopStruct ; func Indiscernibility T -> Equivalence_Relation of the carrier of T means :Def3: :: T_0TOPSP:def 3 for p, q being Point of T holds ( [p,q] in it iff for A being Subset of T st A is open holds ( p in A iff q in A ) ); existence ex b1 being Equivalence_Relation of the carrier of T st for p, q being Point of T holds ( [p,q] in b1 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) proofend; uniqueness for b1, b2 being Equivalence_Relation of the carrier of T st ( for p, q being Point of T holds ( [p,q] in b1 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) ) & ( for p, q being Point of T holds ( [p,q] in b2 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines Indiscernibility T_0TOPSP:def_3_:_ for T being non empty TopStruct for b2 being Equivalence_Relation of the carrier of T holds ( b2 = Indiscernibility T iff for p, q being Point of T holds ( [p,q] in b2 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) ); :: :: Indiscernibility Partition :: definition let T be non empty TopStruct ; func Indiscernible T -> non empty a_partition of the carrier of T equals :: T_0TOPSP:def 4 Class (Indiscernibility T); coherence Class (Indiscernibility T) is non empty a_partition of the carrier of T ; end; :: deftheorem defines Indiscernible T_0TOPSP:def_4_:_ for T being non empty TopStruct holds Indiscernible T = Class (Indiscernibility T); :: :: T_0 Reflex of TopSpace :: definition let T be non empty TopSpace; func T_0-reflex T -> TopSpace equals :: T_0TOPSP:def 5 space (Indiscernible T); correctness coherence space (Indiscernible T) is TopSpace; ; end; :: deftheorem defines T_0-reflex T_0TOPSP:def_5_:_ for T being non empty TopSpace holds T_0-reflex T = space (Indiscernible T); registration let T be non empty TopSpace; cluster T_0-reflex T -> non empty ; coherence not T_0-reflex T is empty ; end; :: :: Function from TopSpace to its T_0 Reflex :: definition let T be non empty TopSpace; func T_0-canonical_map T -> continuous Function of T,(T_0-reflex T) equals :: T_0TOPSP:def 6 Proj (Indiscernible T); coherence Proj (Indiscernible T) is continuous Function of T,(T_0-reflex T) ; end; :: deftheorem defines T_0-canonical_map T_0TOPSP:def_6_:_ for T being non empty TopSpace holds T_0-canonical_map T = Proj (Indiscernible T); theorem Th2: :: T_0TOPSP:2 for T being non empty TopSpace for V being Subset of (T_0-reflex T) holds ( V is open iff union V in the topology of T ) proofend; theorem Th3: :: T_0TOPSP:3 for T being non empty TopSpace for C being set holds ( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) ) proofend; theorem Th4: :: T_0TOPSP:4 for T being non empty TopSpace for p being Point of T holds (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) proofend; theorem Th5: :: T_0TOPSP:5 for T being non empty TopSpace for p, q being Point of T holds ( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T ) proofend; theorem Th6: :: T_0TOPSP:6 for T being non empty TopSpace for A being Subset of T st A is open holds for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds q in A proofend; theorem Th7: :: T_0TOPSP:7 for T being non empty TopSpace for A being Subset of T st A is open holds for C being Subset of T st C in Indiscernible T & C meets A holds C c= A proofend; theorem Th8: :: T_0TOPSP:8 for T being non empty TopSpace holds T_0-canonical_map T is open proofend; Lm1: for T being non empty TopSpace for x, y being Point of (T_0-reflex T) st x <> y holds ex V being Subset of (T_0-reflex T) st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) proofend; :: :: Discernible TopStruct :: definition let T be TopStruct ; redefine attr T is T_0 means :Def7: :: T_0TOPSP:def 7 ( T is empty or for x, y being Point of T st x <> y holds ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ); compatibility ( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) ) proofend; end; :: deftheorem Def7 defines T_0 T_0TOPSP:def_7_:_ for T being TopStruct holds ( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) ); registration cluster non empty TopSpace-like T_0 for TopStruct ; existence ex b1 being TopSpace st ( b1 is T_0 & not b1 is empty ) proofend; end; :: :: T_0 TopSpace :: definition mode T_0-TopSpace is non empty T_0 TopSpace; end; theorem :: T_0TOPSP:9 for T being non empty TopSpace holds T_0-reflex T is T_0-TopSpace proofend; :: :: Homeomorphism of T_0 Reflexes :: theorem :: T_0TOPSP:10 for T, S being non empty TopSpace st ex h being Function of (T_0-reflex S),(T_0-reflex T) st ( h is being_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) holds T,S are_homeomorphic proofend; :: :: Properties of Continuous Mapping from TopSpace to its T_0 Reflex :: theorem Th11: :: T_0TOPSP:11 for T being non empty TopSpace for T0 being T_0-TopSpace for f being continuous Function of T,T0 for p, q being Point of T st [p,q] in Indiscernibility T holds f . p = f . q proofend; theorem Th12: :: T_0TOPSP:12 for T being non empty TopSpace for T0 being T_0-TopSpace for f being continuous Function of T,T0 for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)} proofend; :: :: Factorization :: theorem :: T_0TOPSP:13 for T being non empty TopSpace for T0 being T_0-TopSpace for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T) proofend;