:: by Masami Tanaka , Hiroshi Imura and Yatsuka Nakamura

::

:: Received July 6, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

theorem Th1: :: FINTOPO5:1

for X being set

for Y being non empty set

for f being Function of X,Y

for A being Subset of X st f is one-to-one holds

(f ") .: (f .: A) = A

for Y being non empty set

for f being Function of X,Y

for A being Subset of X st f is one-to-one holds

(f ") .: (f .: A) = A

proof end;

definition

let FT1, FT2 be RelStr ;

let h be Function of FT1,FT2;

end;
let h be Function of FT1,FT2;

attr h is being_homeomorphism means :: FINTOPO5:def 1

( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) );

( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) );

:: deftheorem defines being_homeomorphism FINTOPO5:def 1 :

for FT1, FT2 being RelStr

for h being Function of FT1,FT2 holds

( h is being_homeomorphism iff ( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) ) );

for FT1, FT2 being RelStr

for h being Function of FT1,FT2 holds

( h is being_homeomorphism iff ( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) ) );

theorem Th3: :: FINTOPO5:3

for FT1, FT2 being non empty RelStr

for h being Function of FT1,FT2 st h is being_homeomorphism holds

ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism )

for h being Function of FT1,FT2 st h is being_homeomorphism holds

ex g being Function of FT2,FT1 st

( g = h " & g is being_homeomorphism )

proof end;

theorem Th4: :: FINTOPO5:4

for FT1, FT2 being non empty RelStr

for h being Function of FT1,FT2

for n being Nat

for x being Element of FT1

for y being Element of FT2 st h is being_homeomorphism & y = h . x holds

for z being Element of FT1 holds

( z in U_FT (x,n) iff h . z in U_FT (y,n) )

for h being Function of FT1,FT2

for n being Nat

for x being Element of FT1

for y being Element of FT2 st h is being_homeomorphism & y = h . x holds

for z being Element of FT1 holds

( z in U_FT (x,n) iff h . z in U_FT (y,n) )

proof end;

theorem :: FINTOPO5:5

for FT1, FT2 being non empty RelStr

for h being Function of FT1,FT2

for n being Nat

for x being Element of FT1

for y being Element of FT2 st h is being_homeomorphism & y = h . x holds

for v being Element of FT2 holds

( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )

for h being Function of FT1,FT2

for n being Nat

for x being Element of FT1

for y being Element of FT2 st h is being_homeomorphism & y = h . x holds

for v being Element of FT2 holds

( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )

proof end;

theorem :: FINTOPO5:6

for n being non zero Nat

for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous 0 holds

ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)

for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous 0 holds

ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)

proof end;

theorem Th7: :: FINTOPO5:7

for T being non empty RelStr

for p being Element of T

for k being Nat st T is filled holds

U_FT (p,k) c= U_FT (p,(k + 1))

for p being Element of T

for k being Nat st T is filled holds

U_FT (p,k) c= U_FT (p,(k + 1))

proof end;

theorem Th8: :: FINTOPO5:8

for T being non empty RelStr

for p being Element of T

for k being Nat st T is filled holds

U_FT (p,0) c= U_FT (p,k)

for p being Element of T

for k being Nat st T is filled holds

U_FT (p,0) c= U_FT (p,k)

proof end;

theorem Th9: :: FINTOPO5:9

for n being non zero Nat

for jn, j, k being Nat

for p being Element of (FTSL1 n) st p = jn holds

( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )

for jn, j, k being Nat

for p being Element of (FTSL1 n) st p = jn holds

( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )

proof end;

:: Fixed Point Theorem

theorem :: FINTOPO5:10

for kc, km being Nat

for n being non zero Nat

for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds

ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)

for n being non zero Nat

for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds

ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)

proof end;

definition

let A, B be set ;

let R be Relation of A,B;

let x be set ;

:: original: Im

redefine func Im (R,x) -> Subset of B;

coherence

Im (R,x) is Subset of B

end;
let R be Relation of A,B;

let x be set ;

:: original: Im

redefine func Im (R,x) -> Subset of B;

coherence

Im (R,x) is Subset of B

proof end;

:: 2-dimensional linear FT_Str

definition

let n, m be Nat;

ex b_{1} being Relation of [:(Seg n),(Seg m):] st

for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{1},x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]

for b_{1}, b_{2} being Relation of [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{1},x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{2},x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) holds

b_{1} = b_{2}

end;
func Nbdl2 (n,m) -> Relation of [:(Seg n),(Seg m):] means :Def2: :: FINTOPO5:def 2

for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (it,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):];

existence for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (it,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):];

ex b

for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b

proof end;

uniqueness for b

for i, j being Nat st x = [i,j] holds

Im (b

for i, j being Nat st x = [i,j] holds

Im (b

b

proof end;

:: deftheorem Def2 defines Nbdl2 FINTOPO5:def 2 :

for n, m being Nat

for b_{3} being Relation of [:(Seg n),(Seg m):] holds

( b_{3} = Nbdl2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{3},x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] );

for n, m being Nat

for b

( b

for i, j being Nat st x = [i,j] holds

Im (b

definition

let n, m be Nat;

RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #) is strict RelStr ;

end;
func FTSL2 (n,m) -> strict RelStr equals :: FINTOPO5:def 3

RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);

coherence RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);

RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #) is strict RelStr ;

:: deftheorem defines FTSL2 FINTOPO5:def 3 :

for n, m being Nat holds FTSL2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);

for n, m being Nat holds FTSL2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);

:: 2-dimensional small FT_Str

definition

let n, m be Nat;

ex b_{1} being Relation of [:(Seg n),(Seg m):] st

for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{1},x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]

for b_{1}, b_{2} being Relation of [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{1},x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{2},x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) holds

b_{1} = b_{2}

end;
func Nbds2 (n,m) -> Relation of [:(Seg n),(Seg m):] means :Def4: :: FINTOPO5:def 4

for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (it,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:];

existence for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (it,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:];

ex b

for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b

proof end;

uniqueness for b

for i, j being Nat st x = [i,j] holds

Im (b

for i, j being Nat st x = [i,j] holds

Im (b

b

proof end;

:: deftheorem Def4 defines Nbds2 FINTOPO5:def 4 :

for n, m being Nat

for b_{3} being Relation of [:(Seg n),(Seg m):] holds

( b_{3} = Nbds2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds

for i, j being Nat st x = [i,j] holds

Im (b_{3},x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] );

for n, m being Nat

for b

( b

for i, j being Nat st x = [i,j] holds

Im (b

definition

let n, m be Nat;

RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #) is strict RelStr ;

end;
func FTSS2 (n,m) -> strict RelStr equals :: FINTOPO5:def 5

RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);

coherence RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);

RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #) is strict RelStr ;

:: deftheorem defines FTSS2 FINTOPO5:def 5 :

for n, m being Nat holds FTSS2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);

for n, m being Nat holds FTSS2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);