:: 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-2019 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, XCMPLX_0, NAT_1; requirements SUBSET, NUMERALS, ARITHM, BOOLE; 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;