environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, XXREAL_0, CARD_1, FINSEQ_1, ORDERS_2, TOPS_2, FUNCT_2, FIN_TOPO, STRUCT_0, ARYTM_3, EQREL_1, XCMPLX_0, FINTOPO4, NAT_1, ARYTM_1, TARSKI, COMPLEX1, INT_1, ZFMISC_1, RELAT_2, FINTOPO5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, EQREL_1, FUNCT_2, FINSEQ_1, STRUCT_0, FIN_TOPO, FINTOPO3, ENUMSET1, ORDERS_2, FINTOPO4, COMPLEX1, INT_1;
definitions TARSKI;
theorems NAT_1, NAT_2, ZFMISC_1, INT_1, FUNCT_1, FUNCT_2, FINSEQ_1, ABSVALUE, RELSET_1, XBOOLE_0, XBOOLE_1, UNIFORM1, FINTOPO3, ENUMSET1, FINTOPO4, TARSKI, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XREAL_0, NAT_D, XTUPLE_0;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, CARD_1;
constructors HIDDEN, ENUMSET1, REAL_1, NAT_1, EQREL_1, FIN_TOPO, FINTOPO3, FINTOPO4, NAT_D, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, FIN_TOPO, RELAT_1;
expansions TARSKI, FIN_TOPO;
definition
let n,
m be
Nat;
existence
ex b1 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 (b1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
uniqueness
for b1, b2 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 (b1,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 (b2,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) holds
b1 = b2
end;
::
deftheorem Def2 defines
Nbdl2 FINTOPO5:def 2 :
for n, m being Nat
for b3 being Relation of [:(Seg n),(Seg m):] holds
( b3 = 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 (b3,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] );
definition
let n,
m be
Nat;
func Nbds2 (
n,
m)
-> Relation of
[:(Seg n),(Seg m):] means :
Def4:
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
ex b1 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 (b1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
uniqueness
for b1, b2 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 (b1,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 (b2,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) holds
b1 = b2
end;
::
deftheorem Def4 defines
Nbds2 FINTOPO5:def 4 :
for n, m being Nat
for b3 being Relation of [:(Seg n),(Seg m):] holds
( b3 = 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 (b3,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] );