set TR = TOP-REAL n;
let F be Subset of M; ( F = Fr M iff for p being Point of M holds
( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) )
thus
( F = Fr M implies for p being Point of M holds
( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) )
( ( for p being Point of M holds
( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) ) ) implies F = Fr M )proof
assume A1:
F = Fr M
;
for p being Point of M holds
( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
let p be
Point of
M;
( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
thus
(
p in F implies ex
U being
a_neighborhood of
p ex
h being
Function of
(M | U),
(Tdisk ((0. (TOP-REAL n)),1)) st
(
h is
being_homeomorphism &
h . p in Sphere (
(0. (TOP-REAL n)),1) ) )
( ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) implies p in F )proof
consider W being
a_neighborhood of
p such that A2:
M | W,
Tdisk (
(0. (TOP-REAL n)),1)
are_homeomorphic
by Def3;
A3:
p in Int W
by CONNSP_2:def 1;
assume
p in F
;
ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) )
then consider U being
a_neighborhood of
p,
m being
Nat,
h being
Function of
(M | U),
(Tdisk ((0. (TOP-REAL m)),1)) such that A4:
h is
being_homeomorphism
and A5:
h . p in Sphere (
(0. (TOP-REAL m)),1)
by A1, Th5;
A6:
p in Int U
by CONNSP_2:def 1;
M | U,
Tdisk (
(0. (TOP-REAL m)),1)
are_homeomorphic
by A4, T_0TOPSP:def 1;
then
n = m
by A3, A6, XBOOLE_0:3, A2, BROUWER3:14;
hence
ex
U being
a_neighborhood of
p ex
h being
Function of
(M | U),
(Tdisk ((0. (TOP-REAL n)),1)) st
(
h is
being_homeomorphism &
h . p in Sphere (
(0. (TOP-REAL n)),1) )
by A4, A5;
verum
end;
thus
( ex
U being
a_neighborhood of
p ex
h being
Function of
(M | U),
(Tdisk ((0. (TOP-REAL n)),1)) st
(
h is
being_homeomorphism &
h . p in Sphere (
(0. (TOP-REAL n)),1) ) implies
p in F )
by Th5, A1;
verum
end;
assume A7:
for p being Point of M holds
( p in F iff ex U being a_neighborhood of p ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
; F = Fr M
thus
F c= Fr M
XBOOLE_0:def 10 Fr M c= F
let x be object ; TARSKI:def 3 ( not x in Fr M or x in F )
assume A9:
x in Fr M
; x in F
then reconsider x = x as Point of M ;
consider U being a_neighborhood of x, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that
A10:
h is being_homeomorphism
and
A11:
h . x in Sphere ((0. (TOP-REAL m)),1)
by A9, Th5;
A12:
x in Int U
by CONNSP_2:def 1;
consider W being a_neighborhood of x such that
A13:
M | W, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by Def3;
A14:
x in Int W
by CONNSP_2:def 1;
M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic
by A10, T_0TOPSP:def 1;
then
n = m
by A14, A12, XBOOLE_0:3, A13, BROUWER3:14;
hence
x in F
by A10, A11, A7; verum