begin
:: deftheorem Def1 defines are_separated FINTOPO4:def 1 :
for FT being non empty RelStr
for A, B being Subset of FT holds
( A,B are_separated iff ( A ^b misses B & A misses B ^b ) );
theorem Th1:
theorem
theorem
theorem
theorem
theorem Th6:
theorem
theorem Th8:
theorem
theorem
theorem
theorem Th12:
theorem
:: deftheorem Def2 defines is_continuous FINTOPO4:def 2 :
for FT1, FT2 being non empty RelStr
for f being Function of FT1,FT2
for n being Element of NAT holds
( f is_continuous n iff for x being Element of FT1
for 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 );
theorem
theorem
theorem Th16:
theorem
definition
let n be
Nat;
func Nbdl1 n -> Relation of
(Seg n) means :
Def3:
for
i being
Element of
NAT st
i in Seg n holds
Im it,
i = {i,(max (i -' 1),1),(min (i + 1),n)};
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;
:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :
for n being Nat
for b2 being Relation of (Seg n) holds
( b2 = Nbdl1 n iff for i being Element of NAT st i in Seg n holds
Im b2,i = {i,(max (i -' 1),1),(min (i + 1),n)} );
:: deftheorem Def4 defines FTSL1 FINTOPO4:def 4 :
for n being Nat st n > 0 holds
FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #);
theorem
theorem
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} ) ) );
:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :
for n being Nat st n > 0 holds
FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #);
theorem
theorem