:: T_0TOPSP semantic presentation begin 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 proof let X, Y be non empty set ; ::_thesis: 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 let f be Function of X,Y; ::_thesis: 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 let A be Subset of X; ::_thesis: ( ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds x2 in A ) implies f " (f .: A) = A ) assume A1: for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds x2 in A ; ::_thesis: f " (f .: A) = A for x being set st x in f " (f .: A) holds x in A proof let x be set ; ::_thesis: ( x in f " (f .: A) implies x in A ) assume A2: x in f " (f .: A) ; ::_thesis: x in A then f . x in f .: A by FUNCT_1:def_7; then ex x0 being set st ( x0 in X & x0 in A & f . x = f . x0 ) by FUNCT_2:64; hence x in A by A1, A2; ::_thesis: verum end; then ( A c= f " (f .: A) & f " (f .: A) c= A ) by FUNCT_2:42, TARSKI:def_3; hence f " (f .: A) = A by XBOOLE_0:def_10; ::_thesis: verum end; 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 ); 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 ); 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 ) ) proof defpred S1[ set , set ] means for A being Subset of T st A is open holds ( \$1 in A iff \$2 in A ); consider R being Relation of the carrier of T, the carrier of T such that A1: for p, q being Element of T holds ( [p,q] in R iff S1[p,q] ) from RELSET_1:sch_2(); A2: R is_transitive_in the carrier of T proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of T or not y in the carrier of T or not z in the carrier of T or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume that A3: ( x in the carrier of T & y in the carrier of T & z in the carrier of T ) and A4: [x,y] in R and A5: [y,z] in R ; ::_thesis: [x,z] in R reconsider x9 = x, y9 = y, z9 = z as Element of T by A3; for A being Subset of T st A is open holds ( x9 in A iff z9 in A ) proof let A be Subset of T; ::_thesis: ( A is open implies ( x9 in A iff z9 in A ) ) assume A6: A is open ; ::_thesis: ( x9 in A iff z9 in A ) then ( x9 in A iff y9 in A ) by A1, A4; hence ( x9 in A iff z9 in A ) by A1, A5, A6; ::_thesis: verum end; hence [x,z] in R by A1; ::_thesis: verum end; R is_reflexive_in the carrier of T proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of T or [x,x] in R ) A7: for A being Subset of T st A is open holds ( x in A iff x in A ) ; assume x in the carrier of T ; ::_thesis: [x,x] in R hence [x,x] in R by A1, A7; ::_thesis: verum end; then A8: ( dom R = the carrier of T & field R = the carrier of T ) by ORDERS_1:13; R is_symmetric_in the carrier of T proof let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in the carrier of T or not y in the carrier of T or not [x,y] in R or [y,x] in R ) assume that A9: ( x in the carrier of T & y in the carrier of T ) and A10: [x,y] in R ; ::_thesis: [y,x] in R for A being Subset of T st A is open holds ( y in A iff x in A ) by A1, A9, A10; hence [y,x] in R by A1, A9; ::_thesis: verum end; then reconsider R = R as Equivalence_Relation of the carrier of T by A8, A2, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; take R ; ::_thesis: for p, q being Point of T holds ( [p,q] in R iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) let p, q be Point of T; ::_thesis: ( [p,q] in R iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) thus ( [p,q] in R implies for A being Subset of T st A is open holds ( p in A iff q in A ) ) by A1; ::_thesis: ( ( for A being Subset of T st A is open holds ( p in A iff q in A ) ) implies [p,q] in R ) assume for A being Subset of T st A is open holds ( p in A iff q in A ) ; ::_thesis: [p,q] in R hence [p,q] in R by A1; ::_thesis: verum end; 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 proof let R1, R2 be Equivalence_Relation of the carrier of T; ::_thesis: ( ( for p, q being Point of T holds ( [p,q] in R1 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 R2 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) ) implies R1 = R2 ) assume that A11: for p, q being Point of T holds ( [p,q] in R1 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) and A12: for p, q being Point of T holds ( [p,q] in R2 iff for A being Subset of T st A is open holds ( p in A iff q in A ) ) ; ::_thesis: R1 = R2 let x, y be Point of T; :: according to RELSET_1:def_2 ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) ( [x,y] in R1 iff for A being Subset of T st A is open holds ( x in A iff y in A ) ) by A11; hence ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) by A12; ::_thesis: verum end; 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 ) ) ); 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); 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; 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 ) proof let T be non empty TopSpace; ::_thesis: for V being Subset of (T_0-reflex T) holds ( V is open iff union V in the topology of T ) let V be Subset of (T_0-reflex T); ::_thesis: ( V is open iff union V in the topology of T ) A1: V is Subset of (Indiscernible T) by BORSUK_1:def_7; hereby ::_thesis: ( union V in the topology of T implies V is open ) assume V is open ; ::_thesis: union V in the topology of T then V in the topology of (T_0-reflex T) by PRE_TOPC:def_2; hence union V in the topology of T by A1, BORSUK_1:27; ::_thesis: verum end; assume union V in the topology of T ; ::_thesis: V is open then V in the topology of (space (Indiscernible T)) by A1, BORSUK_1:27; hence V is open by PRE_TOPC:def_2; ::_thesis: verum end; 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) ) proof let T be non empty TopSpace; ::_thesis: 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) ) set TR = T_0-reflex T; set R = Indiscernibility T; let C be set ; ::_thesis: ( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class ((Indiscernibility T),p) ) hereby ::_thesis: ( ex p being Point of T st C = Class ((Indiscernibility T),p) implies C is Point of (T_0-reflex T) ) assume C is Point of (T_0-reflex T) ; ::_thesis: ex p being Point of T st C = Class ((Indiscernibility T),p) then C in the carrier of (T_0-reflex T) ; then C in Indiscernible T by BORSUK_1:def_7; hence ex p being Point of T st C = Class ((Indiscernibility T),p) by EQREL_1:36; ::_thesis: verum end; assume ex p being Point of T st C = Class ((Indiscernibility T),p) ; ::_thesis: C is Point of (T_0-reflex T) then C in Class (Indiscernibility T) by EQREL_1:def_3; hence C is Point of (T_0-reflex T) by BORSUK_1:def_7; ::_thesis: verum end; 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) proof let T be non empty TopSpace; ::_thesis: for p being Point of T holds (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) let p be Point of T; ::_thesis: (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) set F = T_0-canonical_map T; set R = Indiscernibility T; (T_0-canonical_map T) . p in the carrier of (T_0-reflex T) ; then (T_0-canonical_map T) . p in Indiscernible T by BORSUK_1:def_7; then consider y being Element of T such that A1: (T_0-canonical_map T) . p = Class ((Indiscernibility T),y) by EQREL_1:36; p in Class ((Indiscernibility T),y) by A1, BORSUK_1:28; hence (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) by A1, EQREL_1:23; ::_thesis: verum end; 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 ) proof let T be non empty TopSpace; ::_thesis: 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 ) let p, q be Point of T; ::_thesis: ( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T ) set F = T_0-canonical_map T; set R = Indiscernibility T; hereby ::_thesis: ( [q,p] in Indiscernibility T implies (T_0-canonical_map T) . q = (T_0-canonical_map T) . p ) assume (T_0-canonical_map T) . q = (T_0-canonical_map T) . p ; ::_thesis: [q,p] in Indiscernibility T then q in (T_0-canonical_map T) . p by BORSUK_1:28; then q in Class ((Indiscernibility T),p) by Th4; hence [q,p] in Indiscernibility T by EQREL_1:19; ::_thesis: verum end; assume [q,p] in Indiscernibility T ; ::_thesis: (T_0-canonical_map T) . q = (T_0-canonical_map T) . p then Class ((Indiscernibility T),q) = Class ((Indiscernibility T),p) by EQREL_1:35; then (T_0-canonical_map T) . q = Class ((Indiscernibility T),p) by Th4; hence (T_0-canonical_map T) . q = (T_0-canonical_map T) . p by Th4; ::_thesis: verum end; 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 proof let T be non empty TopSpace; ::_thesis: 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 let A be Subset of T; ::_thesis: ( A is open implies 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 ) assume A1: A is open ; ::_thesis: 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 set F = T_0-canonical_map T; let p, q be Point of T; ::_thesis: ( p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q implies q in A ) assume that A2: p in A and A3: (T_0-canonical_map T) . p = (T_0-canonical_map T) . q ; ::_thesis: q in A A4: (T_0-canonical_map T) . p = Class ((Indiscernibility T),p) by Th4; q in (T_0-canonical_map T) . p by A3, BORSUK_1:28; then [q,p] in Indiscernibility T by A4, EQREL_1:19; hence q in A by A1, A2, Def3; ::_thesis: verum end; 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 proof let T be non empty TopSpace; ::_thesis: 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 let A be Subset of T; ::_thesis: ( A is open implies for C being Subset of T st C in Indiscernible T & C meets A holds C c= A ) assume A1: A is open ; ::_thesis: for C being Subset of T st C in Indiscernible T & C meets A holds C c= A set R = Indiscernibility T; let C be Subset of T; ::_thesis: ( C in Indiscernible T & C meets A implies C c= A ) assume that A2: C in Indiscernible T and A3: C meets A ; ::_thesis: C c= A consider y being set such that A4: y in C and A5: y in A by A3, XBOOLE_0:3; consider x being set such that x in the carrier of T and A6: C = Class ((Indiscernibility T),x) by A2, EQREL_1:def_3; for p being set st p in C holds p in A proof let p be set ; ::_thesis: ( p in C implies p in A ) [y,x] in Indiscernibility T by A6, A4, EQREL_1:19; then A7: [x,y] in Indiscernibility T by EQREL_1:6; assume A8: p in C ; ::_thesis: p in A then [p,x] in Indiscernibility T by A6, EQREL_1:19; then [p,y] in Indiscernibility T by A7, EQREL_1:7; hence p in A by A1, A5, A8, Def3; ::_thesis: verum end; hence C c= A by TARSKI:def_3; ::_thesis: verum end; theorem Th8: :: T_0TOPSP:8 for T being non empty TopSpace holds T_0-canonical_map T is open proof let T be non empty TopSpace; ::_thesis: T_0-canonical_map T is open set F = T_0-canonical_map T; for A being Subset of T st A is open holds (T_0-canonical_map T) .: A is open proof set D = Indiscernible T; A1: T_0-canonical_map T = proj (Indiscernible T) by BORSUK_1:def_8; let A be Subset of T; ::_thesis: ( A is open implies (T_0-canonical_map T) .: A is open ) assume A2: A is open ; ::_thesis: (T_0-canonical_map T) .: A is open A3: for C being Subset of T st C in Indiscernible T & C meets A holds C c= A by A2, Th7; set A9 = (T_0-canonical_map T) .: A; (T_0-canonical_map T) .: A is Subset of (Indiscernible T) by BORSUK_1:def_7; then (T_0-canonical_map T) " ((T_0-canonical_map T) .: A) = union ((T_0-canonical_map T) .: A) by A1, EQREL_1:67; then A = union ((T_0-canonical_map T) .: A) by A1, A3, EQREL_1:69; then union ((T_0-canonical_map T) .: A) in the topology of T by A2, PRE_TOPC:def_2; hence (T_0-canonical_map T) .: A is open by Th2; ::_thesis: verum end; hence T_0-canonical_map T is open by Def2; ::_thesis: verum end; 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 ) ) ) proof let T be non empty TopSpace; ::_thesis: 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 ) ) ) set S = T_0-reflex T; set F = T_0-canonical_map T; assume ex x, y being Point of (T_0-reflex T) st ( not x = y & ( for V being Subset of (T_0-reflex T) holds ( not V is open or ( not ( x in V & not y in V ) & not ( y in V & not x in V ) ) ) ) ) ; ::_thesis: contradiction then consider x, y being Point of (T_0-reflex T) such that A1: x <> y and A2: for V being Subset of (T_0-reflex T) st V is open holds ( x in V iff y in V ) ; reconsider x = x, y = y as Point of (space (Indiscernible T)) ; consider p being Point of T such that A3: (T_0-canonical_map T) . p = x by BORSUK_1:29; consider q being Point of T such that A4: (T_0-canonical_map T) . q = y by BORSUK_1:29; for A being Subset of T st A is open holds ( p in A iff q in A ) proof let A be Subset of T; ::_thesis: ( A is open implies ( p in A iff q in A ) ) assume A5: A is open ; ::_thesis: ( p in A iff q in A ) T_0-canonical_map T is open by Th8; then A6: (T_0-canonical_map T) .: A is open by A5, Def2; reconsider F = T_0-canonical_map T as Function of the carrier of T, the carrier of (T_0-reflex T) ; hereby ::_thesis: ( q in A implies p in A ) assume p in A ; ::_thesis: q in A then x in F .: A by A3, FUNCT_2:35; then F . q in F .: A by A2, A4, A6; then ex x being set st ( x in the carrier of T & x in A & F . q = F . x ) by FUNCT_2:64; hence q in A by A5, Th6; ::_thesis: verum end; assume q in A ; ::_thesis: p in A then y in F .: A by A4, FUNCT_2:35; then F . p in F .: A by A2, A3, A6; then ex x being set st ( x in the carrier of T & x in A & F . p = F . x ) by FUNCT_2:64; hence p in A by A5, Th6; ::_thesis: verum end; then [p,q] in Indiscernibility T by Def3; hence contradiction by A1, A3, A4, Th5; ::_thesis: verum end; 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 ) ) ) ) ) proof thus ( not T is T_0 or 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 ) ) ) ) by PRE_TOPC:def_8; ::_thesis: ( ( 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 ) ) ) ) implies T is T_0 ) assume A1: ( 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 ) ) ) ) ; ::_thesis: T is T_0 let x, y be Point of T; :: according to PRE_TOPC:def_8 ::_thesis: ( ex b1 being Element of K10( the carrier of T) st ( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) or x = y ) assume A2: for G being Subset of T st G is open holds ( x in G iff y in G ) ; ::_thesis: x = y percases ( 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 ) ) ) ) by A1; supposeA3: T is empty ; ::_thesis: x = y then x = {} by SUBSET_1:def_1; hence x = y by A3, SUBSET_1:def_1; ::_thesis: verum end; suppose 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 ) ) ) ; ::_thesis: x = y hence x = y by A2; ::_thesis: verum end; end; end; 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 ) proof set T = the non empty TopSpace; take T_0-reflex the non empty TopSpace ; ::_thesis: ( T_0-reflex the non empty TopSpace is T_0 & not T_0-reflex the non empty TopSpace is empty ) for x, y being Point of (T_0-reflex the non empty TopSpace) st x <> y holds ex V being Subset of (T_0-reflex the non empty TopSpace) st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by Lm1; hence ( T_0-reflex the non empty TopSpace is T_0 & not T_0-reflex the non empty TopSpace is empty ) by Def7; ::_thesis: verum end; end; 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 proof let T be non empty TopSpace; ::_thesis: T_0-reflex T is T_0-TopSpace for x, y being Point of (T_0-reflex T) st not x = y holds ex A being Subset of (T_0-reflex T) st ( A is open & ( ( x in A & not y in A ) or ( y in A & not x in A ) ) ) by Lm1; hence T_0-reflex T is T_0-TopSpace by Def7; ::_thesis: verum end; 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 proof let T, S be non empty TopSpace; ::_thesis: ( 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 ) implies T,S are_homeomorphic ) set F = T_0-canonical_map T; set G = T_0-canonical_map S; set TR = T_0-reflex T; set SR = T_0-reflex S; given h being Function of (T_0-reflex S),(T_0-reflex T) such that A1: h is being_homeomorphism and A2: T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ; ::_thesis: T,S are_homeomorphic consider f being Function such that A3: dom f = dom (T_0-canonical_map T) and A4: rng f = dom (h * (T_0-canonical_map S)) and A5: f is one-to-one and A6: T_0-canonical_map T = (h * (T_0-canonical_map S)) * f by A2, CLASSES1:77; A7: dom f = the carrier of T by A3, FUNCT_2:def_1; A8: h is continuous by A1, TOPS_2:def_5; A9: h is one-to-one by A1, TOPS_2:def_5; reconsider f = f as Function of T,S by A4, A7, FUNCT_2:def_1, RELSET_1:4; take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism thus A10: ( dom f = [#] T & rng f = [#] S ) by A4, FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) A11: rng h = [#] (T_0-reflex T) by A1, TOPS_2:def_5; A12: [#] (T_0-reflex S) <> {} ; A13: for A being Subset of S st A is open holds f " A is open proof set g = h * (T_0-canonical_map S); let A be Subset of S; ::_thesis: ( A is open implies f " A is open ) set B = (h * (T_0-canonical_map S)) .: A; A14: h " is continuous by A1, TOPS_2:def_5; assume A15: A is open ; ::_thesis: f " A is open A16: for x1, x2 being Element of S st x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 holds x2 in A proof let x1, x2 be Element of S; ::_thesis: ( x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 implies x2 in A ) assume that A17: x1 in A and A18: (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 ; ::_thesis: x2 in A h . ((T_0-canonical_map S) . x1) = (h * (T_0-canonical_map S)) . x2 by A18, FUNCT_2:15; then h . ((T_0-canonical_map S) . x1) = h . ((T_0-canonical_map S) . x2) by FUNCT_2:15; then (T_0-canonical_map S) . x1 = (T_0-canonical_map S) . x2 by A9, FUNCT_2:19; hence x2 in A by A15, A17, Th6; ::_thesis: verum end; T_0-canonical_map S is open by Th8; then (T_0-canonical_map S) .: A is open by A15, Def2; then A19: (h ") " ((T_0-canonical_map S) .: A) is open by A12, A14, TOPS_2:43; A20: h is onto by A11, FUNCT_2:def_3; h .: ((T_0-canonical_map S) .: A) = (h ") " ((T_0-canonical_map S) .: A) by A9, FUNCT_1:84; then h .: ((T_0-canonical_map S) .: A) is open by A9, A19, A20, TOPS_2:def_4; then A21: (h * (T_0-canonical_map S)) .: A is open by RELAT_1:126; [#] (T_0-reflex T) <> {} ; then A22: (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) is open by A21, TOPS_2:43; (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) = f " ((h * (T_0-canonical_map S)) " ((h * (T_0-canonical_map S)) .: A)) by A6, RELAT_1:146; hence f " A is open by A22, A16, Th1; ::_thesis: verum end; A23: dom h = [#] (T_0-reflex S) by A1, TOPS_2:def_5; A24: for A being Subset of T st A is open holds (f ") " A is open proof set g = (h ") * (T_0-canonical_map T); let A be Subset of T; ::_thesis: ( A is open implies (f ") " A is open ) set B = ((h ") * (T_0-canonical_map T)) .: A; assume A25: A is open ; ::_thesis: (f ") " A is open A26: for x1, x2 being Element of T st x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 holds x2 in A proof let x1, x2 be Element of T; ::_thesis: ( x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 implies x2 in A ) assume that A27: x1 in A and A28: ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 ; ::_thesis: x2 in A (h ") . ((T_0-canonical_map T) . x1) = ((h ") * (T_0-canonical_map T)) . x2 by A28, FUNCT_2:15; then A29: (h ") . ((T_0-canonical_map T) . x1) = (h ") . ((T_0-canonical_map T) . x2) by FUNCT_2:15; h " is one-to-one by A11, A9, TOPS_2:50; then (T_0-canonical_map T) . x1 = (T_0-canonical_map T) . x2 by A29, FUNCT_2:19; hence x2 in A by A25, A27, Th6; ::_thesis: verum end; T_0-canonical_map T = h * ((T_0-canonical_map S) * f) by A6, RELAT_1:36; then (h ") * (T_0-canonical_map T) = ((h ") * h) * ((T_0-canonical_map S) * f) by RELAT_1:36; then (h ") * (T_0-canonical_map T) = (id the carrier of (T_0-reflex S)) * ((T_0-canonical_map S) * f) by A23, A11, A9, TOPS_2:52; then ((h ") * (T_0-canonical_map T)) * (f ") = ((T_0-canonical_map S) * f) * (f ") by FUNCT_2:17; then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (f * (f ")) by RELAT_1:36; then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (id the carrier of S) by A5, A10, TOPS_2:52; then T_0-canonical_map S = ((h ") * (T_0-canonical_map T)) * (f ") by FUNCT_2:17; then A30: (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (f ") " (((h ") * (T_0-canonical_map T)) " (((h ") * (T_0-canonical_map T)) .: A)) by RELAT_1:146; T_0-canonical_map T is open by Th8; then (T_0-canonical_map T) .: A is open by A25, Def2; then A31: h " ((T_0-canonical_map T) .: A) is open by A11, A8, TOPS_2:43; ((h ") * (T_0-canonical_map T)) .: A = (h ") .: ((T_0-canonical_map T) .: A) by RELAT_1:126; then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (T_0-canonical_map S) " (h " ((T_0-canonical_map T) .: A)) by A11, A9, TOPS_2:55; then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) is open by A12, A31, TOPS_2:43; hence (f ") " A is open by A26, A30, Th1; ::_thesis: verum end; thus f is one-to-one by A5; ::_thesis: ( f is continuous & f " is continuous ) [#] S <> {} ; hence f is continuous by A13, TOPS_2:43; ::_thesis: f " is continuous [#] T <> {} ; hence f " is continuous by A24, TOPS_2:43; ::_thesis: verum end; 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 proof let T be non empty TopSpace; ::_thesis: 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 let T0 be T_0-TopSpace; ::_thesis: 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 let f be continuous Function of T,T0; ::_thesis: for p, q being Point of T st [p,q] in Indiscernibility T holds f . p = f . q let p, q be Point of T; ::_thesis: ( [p,q] in Indiscernibility T implies f . p = f . q ) set p9 = f . p; set q9 = f . q; assume that A1: [p,q] in Indiscernibility T and A2: not f . p = f . q ; ::_thesis: contradiction consider V being Subset of T0 such that A3: V is open and A4: ( ( f . p in V & not f . q in V ) or ( f . q in V & not f . p in V ) ) by A2, Def7; set A = f " V; [#] T0 <> {} ; then A5: f " V is open by A3, TOPS_2:43; reconsider f = f as Function of the carrier of T, the carrier of T0 ; q in the carrier of T ; then A6: q in dom f by FUNCT_2:def_1; p in the carrier of T ; then p in dom f by FUNCT_2:def_1; then ( ( p in f " V & not q in f " V ) or ( q in f " V & not p in f " V ) ) by A4, A6, FUNCT_1:def_7; hence contradiction by A1, A5, Def3; ::_thesis: verum end; 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)} proof let T be non empty TopSpace; ::_thesis: 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)} let T0 be T_0-TopSpace; ::_thesis: for f being continuous Function of T,T0 for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)} let f be continuous Function of T,T0; ::_thesis: for p being Point of T holds f .: (Class ((Indiscernibility T),p)) = {(f . p)} let p be Point of T; ::_thesis: f .: (Class ((Indiscernibility T),p)) = {(f . p)} set R = Indiscernibility T; for y being set holds ( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . p)} ) proof let y be set ; ::_thesis: ( y in f .: (Class ((Indiscernibility T),p)) iff y in {(f . p)} ) hereby ::_thesis: ( y in {(f . p)} implies y in f .: (Class ((Indiscernibility T),p)) ) assume y in f .: (Class ((Indiscernibility T),p)) ; ::_thesis: y in {(f . p)} then consider x being set such that A1: x in the carrier of T and A2: x in Class ((Indiscernibility T),p) and A3: y = f . x by FUNCT_2:64; [x,p] in Indiscernibility T by A2, EQREL_1:19; then f . x = f . p by A1, Th11; hence y in {(f . p)} by A3, TARSKI:def_1; ::_thesis: verum end; assume y in {(f . p)} ; ::_thesis: y in f .: (Class ((Indiscernibility T),p)) then A4: y = f . p by TARSKI:def_1; p in Class ((Indiscernibility T),p) by EQREL_1:20; hence y in f .: (Class ((Indiscernibility T),p)) by A4, FUNCT_2:35; ::_thesis: verum end; hence f .: (Class ((Indiscernibility T),p)) = {(f . p)} by TARSKI:1; ::_thesis: verum end; 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) proof let T be non empty TopSpace; ::_thesis: 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) let T0 be T_0-TopSpace; ::_thesis: 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) let f be continuous Function of T,T0; ::_thesis: ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T) set F = T_0-canonical_map T; set R = Indiscernibility T; set TR = T_0-reflex T; defpred S1[ set , set ] means \$2 in f .: \$1; A1: for C being set st C in the carrier of (T_0-reflex T) holds ex y being set st ( y in the carrier of T0 & S1[C,y] ) proof let C be set ; ::_thesis: ( C in the carrier of (T_0-reflex T) implies ex y being set st ( y in the carrier of T0 & S1[C,y] ) ) assume C in the carrier of (T_0-reflex T) ; ::_thesis: ex y being set st ( y in the carrier of T0 & S1[C,y] ) then consider p being Point of T such that A2: C = Class ((Indiscernibility T),p) by Th3; A3: f . p in {(f . p)} by TARSKI:def_1; f .: C = {(f . p)} by A2, Th12; hence ex y being set st ( y in the carrier of T0 & S1[C,y] ) by A3; ::_thesis: verum end; ex h being Function of the carrier of (T_0-reflex T), the carrier of T0 st for C being set st C in the carrier of (T_0-reflex T) holds S1[C,h . C] from FUNCT_2:sch_1(A1); then consider h being Function of the carrier of (T_0-reflex T), the carrier of T0 such that A4: for C being set st C in the carrier of (T_0-reflex T) holds h . C in f .: C ; A5: for p being Point of T holds h . (Class ((Indiscernibility T),p)) = f . p proof let p be Point of T; ::_thesis: h . (Class ((Indiscernibility T),p)) = f . p Class ((Indiscernibility T),p) is Point of (T_0-reflex T) by Th3; then h . (Class ((Indiscernibility T),p)) in f .: (Class ((Indiscernibility T),p)) by A4; then h . (Class ((Indiscernibility T),p)) in {(f . p)} by Th12; hence h . (Class ((Indiscernibility T),p)) = f . p by TARSKI:def_1; ::_thesis: verum end; reconsider h = h as Function of (T_0-reflex T),T0 ; A6: [#] T0 <> {} ; for W being Subset of T0 st W is open holds h " W is open proof let W be Subset of T0; ::_thesis: ( W is open implies h " W is open ) assume W is open ; ::_thesis: h " W is open then A7: f " W is open by A6, TOPS_2:43; set V = h " W; for x being set holds ( x in union (h " W) iff x in f " W ) proof let x be set ; ::_thesis: ( x in union (h " W) iff x in f " W ) hereby ::_thesis: ( x in f " W implies x in union (h " W) ) assume x in union (h " W) ; ::_thesis: x in f " W then consider C being set such that A8: x in C and A9: C in h " W by TARSKI:def_4; consider p being Point of T such that A10: C = Class ((Indiscernibility T),p) by A9, Th3; x in the carrier of T by A8, A10; then A11: x in dom f by FUNCT_2:def_1; [x,p] in Indiscernibility T by A8, A10, EQREL_1:19; then A12: C = Class ((Indiscernibility T),x) by A8, A10, EQREL_1:35; h . C in W by A9, FUNCT_1:def_7; then f . x in W by A5, A8, A12; hence x in f " W by A11, FUNCT_1:def_7; ::_thesis: verum end; assume A13: x in f " W ; ::_thesis: x in union (h " W) then f . x in W by FUNCT_1:def_7; then A14: h . (Class ((Indiscernibility T),x)) in W by A5, A13; Class ((Indiscernibility T),x) is Point of (T_0-reflex T) by A13, Th3; then A15: Class ((Indiscernibility T),x) in h " W by A14, FUNCT_2:38; x in Class ((Indiscernibility T),x) by A13, EQREL_1:20; hence x in union (h " W) by A15, TARSKI:def_4; ::_thesis: verum end; then union (h " W) = f " W by TARSKI:1; then union (h " W) in the topology of T by A7, PRE_TOPC:def_2; hence h " W is open by Th2; ::_thesis: verum end; then reconsider h = h as continuous Function of (T_0-reflex T),T0 by A6, TOPS_2:43; set H = h * (T_0-canonical_map T); for x being set st x in the carrier of T holds f . x = (h * (T_0-canonical_map T)) . x proof let x be set ; ::_thesis: ( x in the carrier of T implies f . x = (h * (T_0-canonical_map T)) . x ) assume A16: x in the carrier of T ; ::_thesis: f . x = (h * (T_0-canonical_map T)) . x then Class ((Indiscernibility T),x) in Class (Indiscernibility T) by EQREL_1:def_3; then A17: Class ((Indiscernibility T),x) in the carrier of (T_0-reflex T) by BORSUK_1:def_7; ( x in dom (T_0-canonical_map T) & (T_0-canonical_map T) . x = Class ((Indiscernibility T),x) ) by A16, Th4, FUNCT_2:def_1; then (h * (T_0-canonical_map T)) . x = h . (Class ((Indiscernibility T),x)) by FUNCT_1:13; then (h * (T_0-canonical_map T)) . x in f .: (Class ((Indiscernibility T),x)) by A4, A17; then (h * (T_0-canonical_map T)) . x in {(f . x)} by A16, Th12; hence f . x = (h * (T_0-canonical_map T)) . x by TARSKI:def_1; ::_thesis: verum end; hence ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T) by FUNCT_2:12; ::_thesis: verum end;