let TS be TopSpace; :: thesis: for SS being non empty TopSpace

for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous holds

f is being_homeomorphism

let SS be non empty TopSpace; :: thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous holds

f is being_homeomorphism

let f be Function of TS,SS; :: thesis: ( TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous implies f is being_homeomorphism )

assume that

A1: TS is compact and

A2: SS is T_2 and

A3: rng f = [#] SS and

A4: f is one-to-one and

A5: f is continuous ; :: thesis: f is being_homeomorphism

A6: dom f = [#] TS by FUNCT_2:def 1;

for P being Subset of TS holds

( P is closed iff f .: P is closed )

for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous holds

f is being_homeomorphism

let SS be non empty TopSpace; :: thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous holds

f is being_homeomorphism

let f be Function of TS,SS; :: thesis: ( TS is compact & SS is T_2 & rng f = [#] SS & f is one-to-one & f is continuous implies f is being_homeomorphism )

assume that

A1: TS is compact and

A2: SS is T_2 and

A3: rng f = [#] SS and

A4: f is one-to-one and

A5: f is continuous ; :: thesis: f is being_homeomorphism

A6: dom f = [#] TS by FUNCT_2:def 1;

for P being Subset of TS holds

( P is closed iff f .: P is closed )

proof

hence
f is being_homeomorphism
by A6, A3, A4, TOPS_2:58; :: thesis: verum
let P be Subset of TS; :: thesis: ( P is closed iff f .: P is closed )

A7: P c= f " (f .: P) by A6, FUNCT_1:76;

thus ( P is closed implies f .: P is closed ) by A1, A2, A3, A5, Th16; :: thesis: ( f .: P is closed implies P is closed )

assume f .: P is closed ; :: thesis: P is closed

then A8: f " (f .: P) is closed by A5;

f " (f .: P) c= P by A4, FUNCT_1:82;

hence P is closed by A8, A7, XBOOLE_0:def 10; :: thesis: verum

end;A7: P c= f " (f .: P) by A6, FUNCT_1:76;

thus ( P is closed implies f .: P is closed ) by A1, A2, A3, A5, Th16; :: thesis: ( f .: P is closed implies P is closed )

assume f .: P is closed ; :: thesis: P is closed

then A8: f " (f .: P) is closed by A5;

f " (f .: P) c= P by A4, FUNCT_1:82;

hence P is closed by A8, A7, XBOOLE_0:def 10; :: thesis: verum