environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, FIN_TOPO;
theorems TARSKI, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, FIN_TOPO, FINTOPO3, RELAT_1, ENUMSET1, XREAL_1, XXREAL_0, ORDINAL1, RELSET_1, XREAL_0, NAT_D;
schemes NAT_1, FUNCT_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, RELAT_1;
constructors HIDDEN, ENUMSET1, NAT_1, EQREL_1, NAT_D, FIN_TOPO, FINTOPO3, FINSEQ_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FIN_TOPO, FINSEQ_1;
expansions TARSKI, FIN_TOPO;
definition
let n be
Nat;
existence
ex b1 being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}
uniqueness
for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds
b1 = b2
end;
definition
let n be
Nat;
func Nbdc1 n -> Relation of
(Seg n) means :
Def5:
for
i being
Element of
NAT st
i in Seg n holds
( ( 1
< i &
i < n implies
Im (
it,
i)
= {i,(i -' 1),(i + 1)} ) & (
i = 1 &
i < n implies
Im (
it,
i)
= {i,n,(i + 1)} ) & ( 1
< i &
i = n implies
Im (
it,
i)
= {i,(i -' 1),1} ) & (
i = 1 &
i = n implies
Im (
it,
i)
= {i} ) );
existence
ex b1 being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) )
uniqueness
for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) ) holds
b1 = b2
end;
::
deftheorem Def5 defines
Nbdc1 FINTOPO4:def 5 :
for n being Nat
for b2 being Relation of (Seg n) holds
( b2 = Nbdc1 n iff for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) );