:: Continuous Mappings between Finite and One-Dimensional Finite Topological
:: Spaces
:: by Hiroshi Imura , Masami Tanaka and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, ORDERS_2, SUBSET_1, CONNSP_1, FIN_TOPO,
XXREAL_0, FINTOPO3, TARSKI, ARYTM_3, ARYTM_1, CARD_1, RELAT_2, FUNCT_1,
STRUCT_0, RELAT_1, NAT_1, FINSEQ_1, ZFMISC_1, FINTOPO4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1,
STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1;
constructors ENUMSET1, NAT_1, EQREL_1, NAT_D, FIN_TOPO, FINTOPO3, FINSEQ_1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, RELAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
definition
let FT be non empty RelStr, A,B be Subset of FT;
pred A,B are_separated means
:: FINTOPO4:def 1
A^b misses B & A misses B^b;
symmetry;
end;
theorem :: FINTOPO4:1
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Finf(A,n) c= Finf(A,m);
theorem :: FINTOPO4:2
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Fcl(A,n) c= Fcl(A,m);
theorem :: FINTOPO4:3
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Fdfl(A,m) c= Fdfl(A,n);
theorem :: FINTOPO4:4
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Fint(A,m) c= Fint(A,n);
theorem :: FINTOPO4:5
for FT being non empty RelStr,A,B being Subset of FT st A,B
are_separated holds B,A are_separated;
theorem :: FINTOPO4:6
for FT being filled non empty RelStr, A,B being Subset of FT st
A,B are_separated holds A misses B;
theorem :: FINTOPO4:7
for FT being non empty RelStr, A,B being Subset of FT st FT is
symmetric holds A,B are_separated iff A^f misses B & A misses (B^f);
theorem :: FINTOPO4:8
for FT being filled non empty RelStr, A,B being Subset of FT st
FT is symmetric & A^b misses B holds A misses (B^b);
theorem :: FINTOPO4:9
for FT being filled non empty RelStr, A,B being Subset of FT st FT
is symmetric & A misses (B^b) holds A^b misses B;
theorem :: FINTOPO4:10
for FT being filled non empty RelStr, A,B being Subset of FT st FT
is symmetric holds A,B are_separated iff A^b misses B;
theorem :: FINTOPO4:11
for FT being filled non empty RelStr, A,B being Subset of FT st FT
is symmetric holds A,B are_separated iff A misses (B^b);
theorem :: FINTOPO4:12
for FT being filled non empty RelStr, IT being Subset of FT st
FT is symmetric holds IT is connected iff (for A, B being Subset of FT st IT =
A \/ B & A,B are_separated holds A = IT or B = IT);
theorem :: FINTOPO4:13
for FT being filled non empty RelStr, B being Subset of FT st FT is
symmetric holds B is connected iff not (ex C being Subset of FT st C<>{} & B\C
<>{} & C c= B & (C^b) misses (B\C));
definition
let FT1,FT2 be non empty RelStr, f be Function of FT1, FT2, n be Nat;
pred f is_continuous n means
:: FINTOPO4:def 2
for x being Element of FT1,y being
Element of FT2 st x in the carrier of FT1 & y=f.x holds f.:(U_FT(x,0)) c= U_FT(
y,n);
end;
theorem :: FINTOPO4:14
for FT1 being non empty RelStr, FT2 being filled non empty RelStr, n
being Element of NAT, f being Function of FT1, FT2 st f is_continuous 0 holds f
is_continuous n;
theorem :: FINTOPO4:15
for FT1 being non empty RelStr, FT2 being filled non empty RelStr,
n0,n being Element of NAT, f being Function of FT1, FT2 st f is_continuous n0 &
n0<=n holds f is_continuous n;
theorem :: FINTOPO4:16
for FT1,FT2 being non empty RelStr, A being Subset of FT1,B
being Subset of FT2, f being Function of FT1, FT2 st f is_continuous 0 & B=f.:A
holds f.:(A^b) c= B^b;
theorem :: FINTOPO4:17
for FT1,FT2 being non empty RelStr,A being Subset of FT1, B being
Subset of FT2, f being Function of FT1, FT2 st A is connected & f is_continuous
0 & B=f.:A holds B is connected;
::1 dimensional linear FT_Str
definition
let n be Nat;
func Nbdl1 n -> Relation of Seg n means
:: FINTOPO4:def 3
for i being Element of NAT st
i in Seg n holds Im(it,i)={i,max(i-'1,1),min(i+1,n)};
end;
definition
let n be Nat;
assume
n>0;
func FTSL1 n -> non empty RelStr equals
:: FINTOPO4:def 4
RelStr(# Seg n,Nbdl1 n #);
end;
theorem :: FINTOPO4:18
for n being Nat st n>0 holds FTSL1 n is filled;
theorem :: FINTOPO4:19
for n being Nat st n>0 holds FTSL1 n is symmetric;
::1 dimensional cyclic FT_Str
definition
let n be Nat;
func Nbdc1 n -> Relation of Seg n means
:: FINTOPO4:def 5
for i being Element of NAT st
i in Seg n holds (1*0;
func FTSC1 n -> non empty RelStr equals
:: FINTOPO4:def 6
RelStr(# Seg n,Nbdc1 n #);
end;
theorem :: FINTOPO4:20
for n being Element of NAT st n>0 holds FTSC1 n is filled;
theorem :: FINTOPO4:21
for n being Element of NAT st n>0 holds FTSC1 n is symmetric;
*