:: Some Set Series in Finite Topological Spaces. {F}undamental Concepts
:: for Image Processing
:: by Masami Tanaka and Yatsuka Nakamura
::
:: Received January 26, 2004
:: Copyright (c) 2004-2026 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 XBOOLE_0, ORDERS_2, SUBSET_1, FIN_TOPO, TARSKI, PRE_TOPC,
FUNCT_1, NUMBERS, ZFMISC_1, STRUCT_0, ARYTM_3, CARD_1, RELAT_1, NAT_1,
FINTOPO3, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FIN_TOPO, PRE_TOPC, STRUCT_0, ORDERS_2;
constructors NAT_1, FIN_TOPO, RELSET_1, NUMBERS;
registrations SUBSET_1, ORDINAL1, RELSET_1, STRUCT_0, FIN_TOPO;
requirements SUBSET, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1;
expansions TARSKI;
theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, FIN_TOPO,
FINTOPO2, ORDINAL1;
schemes RECDEF_1, NAT_1, DOMAIN_1;
begin
reserve T for non empty RelStr,
A,B for Subset of T,
x,x2,y,z for Element of T;
:: The following is definition of "deflation of a set A"
:: (A^f is an inflation of A).
definition
let T;
let A be Subset of T;
func A^d -> Subset of T equals
{x where x is Element of T : for y being
Element of T st y in A` holds not x in U_FT y};
coherence
proof
defpred P[Element of T] means for y st y in A` holds not $1 in U_FT y;
{x:P[x]} is Subset of T from DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th1:
T is filled implies A c= A^f
proof
assume
A1: T is filled;
let x be object;
assume
A2: x in A;
then reconsider y=x as Element of T;
y in U_FT y by A1,FIN_TOPO:def 4;
hence thesis by A2,FIN_TOPO:11;
end;
theorem Th2:
x in A^d iff for y st y in A` holds not x in U_FT y
proof
thus x in A^d implies for y st y in A` holds not x in U_FT y
proof
assume x in A^d;
then ex y st y = x & for z st z in A` holds not y in U_FT z;
hence thesis;
end;
assume for z st z in A` holds not x in U_FT z;
hence thesis;
end;
theorem Th3:
T is filled implies A^d c= A
proof
assume
A1: T is filled;
thus A^d c= A
proof
let x be object;
assume
A2: x in A^d;
then reconsider z=x as Element of T;
now
assume not x in A;
then
A3: x in A` by A2,SUBSET_1:29;
x in U_FT z by A1,FIN_TOPO:def 4;
hence contradiction by A2,A3,Th2;
end;
hence thesis;
end;
end;
theorem Th4:
A^d = ((A`)^f)`
proof
for x being object holds x in A^d iff x in ((A`)^f)`
proof
let x be object;
A1: ((A`)^f)={x2:ex y st y in A` & x2 in U_FT y} by FIN_TOPO:def 12;
thus x in A^d implies x in ((A`)^f)`
proof
A2: (A`)^f={x2:ex y st y in A` & x2 in U_FT y} by FIN_TOPO:def 12;
assume
A3: x in A^d;
then not(ex x2 st x2=x & ex y st y in A` & x2 in U_FT y ) by Th2;
then not x in (A`)^f by A2;
hence thesis by A3,SUBSET_1:29;
end;
assume
A4: x in ((A`)^f)`;
then not x in (A`)^f by XBOOLE_0:def 5;
then for y st y in A` holds not x in U_FT y by A1;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
theorem Th5:
A c= B implies A^f c= B^f
proof
assume
A1: A c= B;
let z be object;
assume z in A^f;
then ex y st y in A & z in U_FT y by FIN_TOPO:11;
hence thesis by A1,FIN_TOPO:11;
end;
theorem Th6:
A c= B implies A^d c= B^d
proof
assume A c= B;
then
A1: B` c= A` by SUBSET_1:12;
let z be object;
assume
A2: z in A^d;
then for y st y in B` holds not z in U_FT y by A1,Th2;
hence thesis by A2;
end;
theorem
(A /\ B)^b c= (A^b) /\ (B^b)
proof
let x be object;
assume
A1: x in (A /\ B)^b;
then reconsider px=x as Point of T;
A2: U_FT px meets (A /\ B) by A1,FIN_TOPO:8;
then U_FT px meets B by XBOOLE_1:74;
then
A3: x in B^b by FIN_TOPO:8;
U_FT px meets A by A2,XBOOLE_1:74;
then x in A^b by FIN_TOPO:8;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem Th8:
(A \/ B)^b = (A^b) \/ (B^b)
proof
thus (A \/ B)^b c= (A^b) \/ (B^b)
proof
let x be object;
assume
A1: x in (A \/ B)^b;
then reconsider px=x as Point of T;
U_FT px meets (A \/ B) by A1,FIN_TOPO:8;
then U_FT px meets A or U_FT px meets B by XBOOLE_1:70;
then x in A^b or x in B^b by FIN_TOPO:8;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A2: x in (A^b) \/ (B^b);
then reconsider px=x as Point of T;
x in A^b or x in B^b by A2,XBOOLE_0:def 3;
then U_FT px meets A or U_FT px meets B by FIN_TOPO:8;
then U_FT px meets (A \/ B) by XBOOLE_1:70;
hence thesis by FIN_TOPO:8;
end;
theorem
(A^i) \/ (B^i) c= (A \/ B)^i
proof
let x be object;
assume
A1: x in (A^i) \/ (B^i);
then reconsider px=x as Point of T;
x in A^i or x in B^i by A1,XBOOLE_0:def 3;
then
A2: U_FT px c= A or U_FT px c= B by FIN_TOPO:7;
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
then U_FT px c= A \/ B by A2;
hence thesis by FIN_TOPO:7;
end;
theorem Th10:
(A^i) /\ (B^i) = (A /\ B)^i
proof
thus (A^i) /\ (B^i) c= (A /\ B)^i
proof
let x be object;
assume
A1: x in (A^i) /\ (B^i);
then reconsider px=x as Point of T;
x in (B^i) by A1,XBOOLE_0:def 4;
then
A2: U_FT px c= B by FIN_TOPO:7;
x in (A^i) by A1,XBOOLE_0:def 4;
then U_FT px c= A by FIN_TOPO:7;
then U_FT px c= A /\ B by A2,XBOOLE_1:19;
hence thesis by FIN_TOPO:7;
end;
let x be object;
assume
A3: x in (A /\ B)^i;
then reconsider px=x as Point of T;
A4: U_FT px c= (A /\ B) by A3,FIN_TOPO:7;
then U_FT px c= B by XBOOLE_1:18;
then
A5: x in B^i by FIN_TOPO:7;
U_FT px c= A by A4,XBOOLE_1:18;
then x in A^i by FIN_TOPO:7;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th11:
(A^f) \/ (B^f) = (A \/ B)^f
proof
A^f c= (A \/ B)^f & B^f c= (A \/ B)^f by Th5,XBOOLE_1:7;
hence (A^f) \/ (B^f) c= (A \/ B)^f by XBOOLE_1:8;
let z be object;
assume z in (A \/ B)^f;
then consider y such that
A1: y in A \/ B and
A2: z in U_FT y by FIN_TOPO:11;
per cases by A1,XBOOLE_0:def 3;
suppose
y in A;
then z in (A^f) by A2,FIN_TOPO:11;
hence thesis by XBOOLE_0:def 3;
end;
suppose
y in B;
then z in (B^f) by A2,FIN_TOPO:11;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th12:
(A^d) /\ (B^d) = (A /\ B)^d
proof
A1: B^d = ((B`)^f)` by Th4;
thus (A^d) /\ (B^d) = (((A`)^f)`) /\ (B^d) by Th4
.= (((A`)^f) \/ ((B`)^f))` by A1,XBOOLE_1:53
.= ((A` \/ B`)^f)` by Th11
.= (((A /\ B)`)^f)` by XBOOLE_1:54
.= (A /\ B)^d by Th4;
end;
definition
let T be non empty RelStr;
let A be Subset of T;
func Fcl(A) -> sequence of bool the carrier of T means
:Def2:
(for n being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^b)
& it.0=A;
existence
proof
defpred P[set,set,set] means for B being Subset of T st B=$2 holds $3=B^b;
A1: for n being Nat for x being Subset of T ex y being Subset
of T st P[n,x,y]
proof
let n be Nat,x be Subset of T;
reconsider C=x as Subset of T;
P[n,x,C^b];
hence thesis;
end;
ex f being sequence of bool(the carrier of T) st f.0 = A & for n
being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let f1,f2 be sequence of bool(the carrier of T) such that
A2: for n being Nat,B being Subset of T st B=f1.n holds f1.
(n+1) =B^b and
A3: f1.0=A and
A4: for n being Nat,B being Subset of T st B=f2.n holds f2.
( n+1)=B^b and
A5: f2.0=A;
defpred P[Nat] means f1.$1=f2.$1;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A7: P[n];
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider B1=f1.n as Subset of T;
B1^b=f1.(n+1) by A2;
hence thesis by A4,A7;
end;
A8: dom f1=NAT by FUNCT_2:def 1;
then
A9: dom f1=dom f2 by FUNCT_2:def 1;
A10: P[0] by A3,A5;
for n being Nat holds P[n] from NAT_1:sch 2(A10,A6);
then for x being object st x in dom f1 holds f1.x=f2.x by A8;
hence f1=f2 by A9,FUNCT_1:2;
end;
end;
definition
let T be non empty RelStr;
let A be Subset of T, n be Nat;
func Fcl(A,n) -> Subset of T equals
(Fcl A).n;
coherence
proof
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
(Fcl A).n9 c= the carrier of T;
hence thesis;
end;
end;
definition
let T be non empty RelStr;
let A be Subset of T;
func Fint(A) -> sequence of bool the carrier of T means
:Def4:
(for n
being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^i) & it.0=A;
existence
proof
defpred P[set,set,set] means for B being Subset of T st B=$2 holds $3=B^i;
A1: for n being Nat for x being Subset of T ex y being Subset
of T st P[n,x,y]
proof
let n be Nat,x be Subset of T;
reconsider C=x as Subset of T;
for B being Subset of T st B=x holds C^i=B^i;
hence thesis;
end;
ex f being sequence of bool(the carrier of T) st f.0 = A & for n
being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A1 );
hence thesis;
end;
uniqueness
proof
let f1,f2 be sequence of bool(the carrier of T) such that
A2: for n being Nat,B being Subset of T st B=f1.n holds f1.
(n+1) =B^i and
A3: f1.0=A and
A4: for n being Nat,B being Subset of T st B=f2.n holds f2.
( n+1)=B^i and
A5: f2.0=A;
defpred P[Nat] means f1.$1=f2.$1;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A7: P[n];
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider B1=f1.n as Subset of T;
B1^i=f1.(n+1) by A2;
hence thesis by A4,A7;
end;
A8: dom f1=NAT by FUNCT_2:def 1;
then
A9: dom f1=dom f2 by FUNCT_2:def 1;
A10: P[0] by A3,A5;
for n being Nat holds P[n] from NAT_1:sch 2(A10,A6);
then for x being object st x in dom f1 holds f1.x=f2.x by A8;
hence f1=f2 by A9,FUNCT_1:2;
end;
end;
definition
let T be non empty RelStr;
let A be Subset of T, n be Nat;
func Fint(A,n) -> Subset of T equals
(Fint A).n;
coherence
proof
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
(Fint A).n9 c= the carrier of T;
hence thesis;
end;
end;
theorem
for n being Nat holds Fcl(A,n+1) = (Fcl(A,n))^b by Def2;
theorem
Fcl(A,0) = A by Def2;
theorem Th15:
Fcl(A,1) = A^b
proof
(Fcl A).0=A by Def2;
then (Fcl A).(0+1)=A^b by Def2;
hence thesis;
end;
theorem
Fcl(A,2) = A^b^b
proof
for B being Subset of T st B=(Fcl A).1 holds (Fcl A).(1+1)=B^b by Def2;
then Fcl(A,2)=(Fcl(A,1))^b .=(A^b)^b by Th15;
hence thesis;
end;
theorem Th17:
for n being Nat holds Fcl(A \/ B,n) = Fcl(A,n) \/ Fcl (B,n)
proof
let n be Nat;
for n being Nat holds (Fcl(A \/ B)).n = (Fcl A).n \/ (Fcl B). n
proof
defpred P[Nat] means (Fcl(A \/ B)).$1 = (Fcl A).$1 \/ (Fcl B).
$1;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
(Fcl(A \/ B)).(k+1) = Fcl(A \/ B,k)^b by Def2
.= Fcl(A,k)^b \/ Fcl(B,k)^b by A2,Th8
.= Fcl(A,k+1) \/ Fcl(B,k)^b by Def2
.= (Fcl(A)).(k+1) \/ (Fcl(B)).(k+1) by Def2;
hence thesis;
end;
(Fcl(A \/ B)).0 = A \/ B by Def2
.= (Fcl A).0 \/ B by Def2
.= (Fcl A).0 \/ (Fcl B).0 by Def2;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
hence thesis;
end;
theorem
for n being Nat holds Fint(A,n+1) = (Fint(A,n))^i by Def4;
theorem
Fint(A,0) = A by Def4;
theorem Th20:
Fint(A,1) = A^i
proof
(Fint A).0=A & for B being Subset of T st B=(Fint A).0 holds (Fint A).(0
+1)= B^i by Def4;
hence thesis;
end;
theorem
Fint(A,2) = A^i^i
proof
thus Fint(A,2)=Fint(A,1+1) .=(Fint(A,1))^i by Def4
.=A^i^i by Th20;
end;
theorem Th22:
for n being Nat holds Fint(A /\ B,n) = Fint(A,n) /\ Fint(B,n)
proof
defpred P[Nat] means (Fint(A /\ B)).$1 = (Fint A).$1 /\ (Fint B).
$1;
let n be Nat;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
(Fint(A /\ B)).(k+1) = Fint(A /\ B,k)^i by Def4
.= ((Fint(A,k))^i) /\ (Fint(B,k)^i) by A2,Th10
.= Fint(A,k+1) /\ ((Fint(B,k))^i) by Def4
.= (Fint A).(k+1) /\ (Fint B).(k+1) by Def4;
hence thesis;
end;
(Fint(A /\ B)).0 = A /\ B by Def4
.= (Fint(A)).0 /\ B by Def4
.= (Fint(A)).0 /\ (Fint(B)).0 by Def4;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds A c= Fcl(A,n)
proof
defpred P[Nat] means A c= (Fcl A).$1;
assume
A1: T is filled;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then A^b c= Fcl(A,k)^b by FIN_TOPO:14;
then
A3: A^b c= Fcl(A,k+1) by Def2;
A c= A^b by A1,FIN_TOPO:13;
hence thesis by A3,XBOOLE_1:1;
end;
let n be Nat;
A4: P[0] by Def2;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds Fint(A,n) c= A
proof
defpred P[Nat] means (Fint A).$1 c= A;
assume
A1: T is filled;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then Fint(A,k)^i c= A^i by FINTOPO2:1;
then
A3: Fint(A,k+1) c= A^i by Def4;
A^i c= A by A1,FIN_TOPO:22;
hence thesis by A3,XBOOLE_1:1;
end;
let n be Nat;
A4: P[0] by Def4;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds Fcl(A,n) c= Fcl(A ,n+1)
proof
assume
A1: T is filled;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
((Fcl A).n)^b = Fcl(A,n+1) by Def2;
hence thesis by A1,FIN_TOPO:13;
end;
theorem
T is filled implies for n being Nat holds Fint(A,n+1) c= Fint(A,n)
proof
assume
A1: T is filled;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
((Fint A).n)^i = Fint(A,n+1) by Def4;
hence thesis by A1,FIN_TOPO:22;
end;
theorem Th27:
for n being Nat holds Fint(A`,n)` = Fcl(A,n)
proof
defpred P[Nat] means Fint(A`,$1)` = Fcl(A,$1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
Fcl(A,k+1) = Fcl(A,k)^b by Def2
.= ((Fint(A`,k)``)^i)` by A2,FIN_TOPO:16
.= Fint(A`,k+1)` by Def4;
hence thesis;
end;
Fint(A`,0)` = A`` by Def4
.= Fcl(A,0) by Def2;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th28:
for n being Nat holds Fcl(A`,n)` = Fint(A,n)
proof
let n be Nat;
Fint(A,n) = Fint(A``,n)`` .= Fcl(A`,n)` by Th27;
hence thesis;
end;
theorem
for n being Nat holds Fcl(A,n) \/ Fcl(B,n) = Fint((A \/ B)` ,n)`
proof
let n be Nat;
Fcl(A,n) \/ Fcl(B,n) = Fcl(A \/ B,n) by Th17
.= Fint((A \/ B)`,n)` by Th27;
hence thesis;
end;
theorem
for n being Nat holds Fint(A,n) /\ Fint(B,n) = Fcl((A /\ B) `,n)`
proof
let n be Nat;
Fint(A,n) /\ Fint(B,n) = Fint(A /\ B,n) by Th22
.= Fcl((A /\ B)`,n)` by Th28;
hence thesis;
end;
:: Function of Inflation Series
definition
let T be non empty RelStr;
let A be Subset of T;
func Finf(A) -> sequence of bool(the carrier of T) means
:Def6:
(for n
being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^f) & it.0=A;
existence
proof
defpred P[set,set,set] means (for B being Subset of T st B=$2 holds $3=B^f
);
A1: for n being Nat for x being Subset of T ex y being Subset
of T st P[n,x,y]
proof
let n be Nat,x be Subset of T;
reconsider C=x as Subset of T;
for B being Subset of T st B=x holds C^f=B^f;
hence thesis;
end;
ex f being sequence of bool(the carrier of T) st f.0 = A & for n
being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A1 );
hence thesis;
end;
uniqueness
proof
let f1,f2 be sequence of bool(the carrier of T) such that
A2: for n being Nat,B being Subset of T st B=f1.n holds f1.
(n+1) =B^f and
A3: f1.0=A and
A4: for n being Nat,B being Subset of T st B=f2.n holds f2.
( n+1)=B^f and
A5: f2.0=A;
defpred P[Nat] means f1.$1=f2.$1;
A6: dom f1=NAT by FUNCT_2:def 1;
then
A7: dom f1=dom f2 by FUNCT_2:def 1;
for n being Nat holds P[n]
proof
let n be Nat;
A8: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A9: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider B1=f1.k as Subset of T;
B1^f=f1.(k+1) by A2;
hence thesis by A4,A9;
end;
A10: P[0] by A3,A5;
for m being Nat holds P[m] from NAT_1:sch 2(A10,A8);
hence thesis;
end;
then for x being object st x in dom f1 holds f1.x=f2.x by A6;
hence f1=f2 by A7,FUNCT_1:2;
end;
end;
definition
let T be non empty RelStr;
let A be Subset of T, n be Nat;
func Finf(A,n) -> Subset of T equals
(Finf A).n;
coherence
proof
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
(Finf A).n9 c= the carrier of T;
hence thesis;
end;
end;
:: Function of Deflation Series
definition
let T be non empty RelStr;
let A be Subset of T;
func Fdfl(A) -> sequence of bool(the carrier of T) means
:Def8:
(for n
being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^d) & it.0=A;
existence
proof
defpred P[set,set,set] means for B being Subset of T st B=$2 holds $3=B^d;
A1: for n being Nat for x being Subset of T ex y being Subset
of T st P[n,x,y]
proof
let n be Nat,x be Subset of T;
for B being Subset of T st B=x holds x^d=B^d;
hence thesis;
end;
ex f being sequence of bool(the carrier of T) st f.0 = A & for n
being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let f1,f2 be sequence of bool(the carrier of T) such that
A2: for n being Nat,B being Subset of T st B=f1.n holds f1.
(n+1) =B^d and
A3: f1.0=A and
A4: for n being Nat,B being Subset of T st B=f2.n holds f2.
( n+1)=B^d and
A5: f2.0=A;
defpred P[Nat] means f1.$1=f2.$1;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A7: P[n];
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider B1=f1.n as Subset of T;
B1^d=f1.(n+1) by A2;
hence thesis by A4,A7;
end;
A8: dom f1=NAT by FUNCT_2:def 1;
then
A9: dom f1=dom f2 by FUNCT_2:def 1;
A10: P[0] by A3,A5;
for n being Nat holds P[n] from NAT_1:sch 2(A10,A6);
then for x being object st x in dom f1 holds f1.x=f2.x by A8;
hence f1=f2 by A9,FUNCT_1:2;
end;
end;
definition
let T be non empty RelStr;
let A be Subset of T, n be Nat;
func Fdfl(A,n) -> Subset of T equals
(Fdfl A).n;
coherence
proof
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
(Fdfl A).n9 c= the carrier of T;
hence thesis;
end;
end;
theorem
for n being Nat holds Finf(A,n+1) = (Finf(A,n))^f by Def6;
theorem
Finf(A,0) = A by Def6;
theorem Th33:
Finf(A,1) = A^f
proof
(Finf A).0=A & for B being Subset of T st B=(Finf A).0 holds (Finf A).(0
+1)= B^f by Def6;
hence thesis;
end;
theorem
Finf(A,2) = A^f^f
proof
Finf(A,2)=Finf(A,1+1) .=(Finf(A,1))^f by Def6
.=A^f^f by Th33;
hence thesis;
end;
theorem
for n being Nat holds Finf(A \/ B,n) = Finf(A,n) \/ Finf(B, n)
proof
defpred P[Nat] means (Finf(A \/ B)).$1 = (Finf(A)).$1 \/ (Finf B)
.$1;
let n be Nat;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
(Finf(A \/ B)).(k+1) = Finf(A \/ B,k)^f by Def6
.= Finf(A,k)^f \/ Finf(B,k)^f by A2,Th11
.= Finf(A,k+1) \/ Finf(B,k)^f by Def6
.= (Finf(A)).(k+1) \/ (Finf(B)).(k+1) by Def6;
hence thesis;
end;
(Finf(A \/ B)).0 = A \/ B by Def6
.= (Finf(A)).0 \/ B by Def6
.= (Finf(A)).0 \/ (Finf(B)).0 by Def6;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds A c= Finf(A,n)
proof
defpred P[Nat] means A c= (Finf A).$1;
assume
A1: T is filled;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then A^f c= Finf(A,k)^f by Th5;
then
A3: A^f c= Finf(A,k+1) by Def6;
A c= A^f by A1,Th1;
hence thesis by A3,XBOOLE_1:1;
end;
let n be Nat;
A4: P[0] by Def6;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds Finf(A,n) c= Finf
(A,n+1)
proof
assume
A1: T is filled;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
((Finf A).n)^f = Finf(A,n+1) by Def6;
hence thesis by A1,Th1;
end;
theorem
for n being Nat holds Fdfl(A,n+1) = (Fdfl(A,n))^d by Def8;
theorem
Fdfl(A,0) = A by Def8;
theorem Th40:
Fdfl(A,1) = A^d
proof
(Fdfl A).0=A & for B being Subset of T st B=(Fdfl A).0 holds (Fdfl(A)).(
0+1) =B^d by Def8;
hence thesis;
end;
theorem
Fdfl(A,2) = A^d^d
proof
Fdfl(A,2)=Fdfl(A,1+1) .=(Fdfl(A,1))^d by Def8;
hence thesis by Th40;
end;
theorem Th42:
for n being Nat holds Fdfl(A /\ B,n) = Fdfl(A,n) /\ Fdfl(B,n)
proof
defpred P[Nat] means (Fdfl(A /\ B)).$1= (Fdfl A).$1 /\ (Fdfl B).
$1;
let n be Nat;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
(Fdfl(A /\ B)).(k+1) = Fdfl(A /\ B,k)^d by Def8
.= ((Fdfl(A,k))^d) /\ ((Fdfl(B,k))^d) by A2,Th12
.= Fdfl(A,k+1) /\ ((Fdfl(B,k))^d) by Def8
.= (Fdfl A).(k+1) /\ (Fdfl B).(k+1) by Def8;
hence thesis;
end;
(Fdfl(A /\ B)).0 = A /\ B by Def8
.= (Fdfl A).0 /\ B by Def8
.= (Fdfl A).0 /\ (Fdfl B).0 by Def8;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds Fdfl(A,n) c= A
proof
defpred P[Nat] means (Fdfl(A)).$1 c= A;
assume
A1: T is filled;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then Fdfl(A,k)^d c= A^d by Th6;
then
A3: Fdfl(A,k+1) c= A^d by Def8;
A^d c= A by A1,Th3;
hence thesis by A3,XBOOLE_1:1;
end;
let n be Nat;
A4: P[0] by Def8;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
T is filled implies for n being Nat holds Fdfl(A,n+1) c= Fdfl(A,n)
proof
assume
A1: T is filled;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
((Fdfl A).n)^d = Fdfl(A,n+1) by Def8;
hence thesis by A1,Th3;
end;
theorem Th45:
for n being Nat holds Fdfl(A,n) = Finf(A`,n)`
proof
defpred P[Nat] means (Fdfl(A)).$1= ((Finf(A`)).In($1,NAT))`;
let n be Nat;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A2: P[k];
(Fdfl A).(k+1) = Fdfl(A,k)^d by Def8;
then (Fdfl A).(k+1) = ((((Fdfl(A)).kk)`)^f)` by Th4
.= ((Finf(A`)).In(k+1,NAT))` by A2,Def6;
hence thesis;
end;
((Finf(A`)).0)` = A`` by Def6
.= A;
then
A3: P[0] by Def8;
reconsider n as Element of NAT by ORDINAL1:def 12;
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
then P[n];
hence thesis;
end;
theorem
for n being Nat holds Fdfl(A,n) /\ Fdfl(B,n) = Finf((A /\ B )`,n)`
proof
let n be Nat;
Fdfl(A,n) /\ Fdfl(B,n) = Fdfl(A /\ B,n) by Th42
.= Finf((A /\ B)`,n)` by Th45;
hence thesis;
end;
definition :: n-th neighbourhood of x
let T be non empty RelStr, n be Nat, x be Element of T;
func U_FT(x,n) -> Subset of T equals
Finf((U_FT x),n);
coherence;
end;
theorem
U_FT(x,0) = U_FT x by Def6;
theorem
for n being Nat holds U_FT(x,n+1) = (U_FT(x,n))^f by Def6;
definition
let S, T be non empty RelStr;
pred S, T are_mutually_symmetric means
the carrier of S = the carrier of T &
for x being Element of S, y being Element of T holds y in U_FT x iff x in U_FT
y;
symmetry;
end;