let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L holds
f is being_homeomorphism
let f be Function of S,T; :: thesis: ( f is bijective & ex K being Basis of S ex L being Basis of T st f .: K = L implies f is being_homeomorphism )
assume A1: f is bijective ; :: thesis: ( for K being Basis of S
for L being Basis of T holds not f .: K = L or f is being_homeomorphism )
given K being Basis of S, L being Basis of T such that A2: f .: K = L ; :: thesis: f is being_homeomorphism
for W being Subset of T st W in L holds
f " W is open
proof
let W be Subset of T; :: thesis: ( W in L implies f " W is open )
assume W in L ; :: thesis: f " W is open
then consider V being Subset of S such that
A3: ( V in K & W = f .: V ) by A2, FUNCT_2:def 10;
dom f = the carrier of S by FUNCT_2:def 1;
then V = f " W by A1, A3, FUNCT_1:94;
hence f " W is open by A3, TOPS_2:def 1; :: thesis: verum
end;
then A4: f is continuous by YELLOW_9:34;
for V being Subset of S st V in K holds
f .: V is open
proof
let V be Subset of S; :: thesis: ( V in K implies f .: V is open )
assume V in K ; :: thesis: f .: V is open
then f .: V in f .: K by FUNCT_2:def 10;
hence f .: V is open by A2, TOPS_2:def 1; :: thesis: verum
end;
then f is open by Th45;
then A5: f " is continuous by A1, TOPREALA:14;
A6: rng f = the carrier of T by A1, FUNCT_2:def 3
.= [#] T by STRUCT_0:def 3 ;
dom f = the carrier of S by FUNCT_2:def 1
.= [#] S by STRUCT_0:def 3 ;
hence f is being_homeomorphism by A1, A5, A4, A6, TOPS_2:def 5; :: thesis: verum