Copyright (c) 2000 Association of Mizar Users
environ
vocabulary FIN_TOPO, BOOLE, SUBSET_1, PRE_TOPC, MARGREL1, FUNCT_1, FINTOPO2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, FUNCT_1, FUNCT_2,
FIN_TOPO, PRE_TOPC, MARGREL1;
constructors DOMAIN_1, FIN_TOPO, PRE_TOPC, MARGREL1;
clusters SUBSET_1, RELSET_1, STRUCT_0, FIN_TOPO, PRE_TOPC, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, STRUCT_0, XBOOLE_0;
theorems TARSKI, SUBSET_1, FIN_TOPO, STRUCT_0, FUNCT_2, MARGREL1, XBOOLE_0,
XBOOLE_1;
schemes COMPLSP1, SUPINF_2;
begin
::
:: SECTION1 : Some Useful Theorems on Finite Topological Spaces
::
reserve FT for non empty FT_Space_Str;
reserve A for Subset of FT;
theorem
for FT being non empty FT_Space_Str,
A,B being Subset of FT holds
A c= B implies A^i c= B^i
proof
let FT be non empty FT_Space_Str;
let A,B be Subset of FT;
assume A1:A c= B;
let x be set;
assume A2:x in A^i;
then reconsider y=x as Element of FT;
A3:U_FT y c= A by A2,FIN_TOPO:12;
for t being Element of FT st t in U_FT y holds t in B
proof
let t be Element of FT;
assume t in U_FT y;
then t in A by A3;
hence t in B by A1;
end;
then U_FT y c= B by SUBSET_1:7;
hence thesis by FIN_TOPO:12;
end;
theorem Th2:
A^delta = (A^b) /\ ((A^i)`)
proof
for x being set holds x in A^delta iff x in (A^b) /\ ((A^i)`)
proof
let x be set;
thus x in A^delta implies x in (A^b) /\ ((A^i)`)
proof
assume A1:x in A^delta;
then reconsider y=x as Element of FT;
U_FT y meets A & U_FT y meets A` by A1,FIN_TOPO:10;
then y in (A^b) & y in ((A`)^b)`` by FIN_TOPO:13;
then y in (A^b) & y in ((A^i)`) by FIN_TOPO:23;
hence x in ((A^b) /\ ((A^i)`)) by XBOOLE_0:def 3;
end;
assume A2: x in ((A^b) /\ ((A^i)`));
then reconsider y=x as Element of FT;
x in (A^b) & x in ((A^i)`) by A2,XBOOLE_0:def 3;
then x in (A^b) & x in ((((A`)^b)`)`) by FIN_TOPO:23;
then U_FT y meets A & U_FT y meets A` by FIN_TOPO:13;
hence x in A^delta by FIN_TOPO:10;
end;
hence thesis by TARSKI:2;
end;
theorem
A^delta = A^b \ A^i
proof
for x being set holds x in A^delta iff x in A^b \ A^i
proof
let x be set;
thus x in A^delta implies x in A^b \ A^i
proof
assume x in A^delta;
then x in ((A^b) /\ ((A^i)`)) by Th2;
hence thesis by SUBSET_1:32;
end;
assume x in A^b \ A^i;
then x in ((A^b) /\ ((A^i)`)) by SUBSET_1:32;
hence thesis by Th2;
end;
hence thesis by TARSKI:2;
end;
theorem
A` is open implies A is closed
proof
assume A` is open;
then A1:(A`) = (A`)^i by FIN_TOPO:def 15;
(A`)^i = (((A`)`)^b)` by FIN_TOPO:23
.= (A^b)`;
then A = (A^b)`` by A1
.= A^b;
hence thesis by FIN_TOPO:def 16;
end;
theorem
A` is closed implies A is open
proof
assume A` is closed;
then A1:(A`) = (A`)^b by FIN_TOPO:def 16;
(A`)^b = (((A`)`)^i)` by FIN_TOPO:22
.= (A^i)`;
then A = (A^i)`` by A1
.= A^i;
hence thesis by FIN_TOPO:def 15;
end;
definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
let A be Subset of FT;
func P_1(x,y,A) -> Element of BOOLEAN equals
:Def1:
TRUE if (y in U_FT x) & (y in A)
otherwise FALSE;
correctness;
end;
definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
let A be Subset of FT;
func P_2(x,y,A) -> Element of BOOLEAN equals
:Def2:
TRUE if (y in U_FT x) & (y in A`)
otherwise FALSE;
correctness;
end;
theorem
for x,y be Element of FT, A be Subset of FT
holds P_1(x,y,A) = TRUE iff (y in U_FT x) & (y in A) by Def1,MARGREL1:38;
theorem
for x,y be Element of FT, A be Subset of FT
holds P_2(x,y,A) = TRUE iff (y in U_FT x) & (y in A`) by Def2,MARGREL1:38;
theorem Th8:
for x be Element of FT, A be Subset of FT
holds x in A^delta iff ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE
proof
let x be Element of FT;
let A be Subset of FT;
A1:x in A^delta implies ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE
proof
assume A2:x in A^delta;
reconsider z=x as Element of FT;
A3:U_FT z meets A & U_FT z meets A` by A2,FIN_TOPO:10;
then consider w1 be set such that
A4:w1 in U_FT z & w1 in A by XBOOLE_0:3;
reconsider w1 as Element of FT by A4;
take w1;
consider w2 be set such that
A5:w2 in U_FT z & w2 in A` by A3,XBOOLE_0:3;
take w2;
thus thesis by A4,A5,Def1,Def2;
end;
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE)
implies x in A^delta
proof
given y1,y2 being Element of FT
such that A6:P_1(x,y1,A)=TRUE and
A7:P_2(x,y2,A)=TRUE;
(y1 in U_FT x) & (y1 in A) by A6,Def1,MARGREL1:38;
then U_FT x /\ A <> {} by XBOOLE_0:def 3;
then A8:U_FT x meets A by XBOOLE_0:def 7;
(y2 in U_FT x) & (y2 in A`) by A7,Def2,MARGREL1:38;
then U_FT x meets A` by XBOOLE_0:3;
hence thesis by A8,FIN_TOPO:10;
end;
hence thesis by A1;
end;
definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
func P_0(x,y) -> Element of BOOLEAN equals
:Def3:
TRUE if y in U_FT x
otherwise FALSE;
correctness;
end;
theorem
for x,y be Element of FT holds
P_0(x,y)=TRUE iff y in U_FT x by Def3,MARGREL1:38;
theorem
for x be Element of FT, A be Subset of FT
holds x in A^i iff (for y be Element of FT holds
(P_0(x,y)=TRUE implies P_1(x,y,A)=TRUE))
proof
let x be Element of FT;
let A be Subset of FT;
A1:x in A^i implies
(for y be Element of FT
holds (P_0(x,y)=TRUE implies P_1(x,y,A)=TRUE))
proof
assume A2:x in A^i;
let y be Element of FT;
assume A3:P_0(x,y)=TRUE;
A4:U_FT x c= A by A2,FIN_TOPO:12;
y in U_FT x by A3,Def3,MARGREL1:38;
hence thesis by A4,Def1;
end;
(for y be Element of FT
holds (P_0(x,y)=TRUE implies P_1(x,y,A)=TRUE))
implies x in A^i
proof
assume A5:for y be Element of FT holds
(P_0(x,y)=TRUE implies P_1(x,y,A)=TRUE);
for y be Element of FT holds
(y in (U_FT x)) implies ((y in U_FT x) & (y in A))
proof
let y be Element of FT;
assume y in (U_FT x);
then P_0(x,y)=TRUE by Def3;
then P_1(x,y,A)=TRUE by A5;
hence thesis by Def1,MARGREL1:38;
end;
then for y be Element of FT holds
y in (U_FT x) implies (y in A);
then (U_FT x) c= A by SUBSET_1:7;
hence thesis by FIN_TOPO:12;
end;
hence thesis by A1;
end;
theorem
for x be Element of FT, A be Subset of FT
holds
x in A^b iff
ex y1 being Element of FT
st P_1(x,y1,A)=TRUE
proof
let x be Element of FT;
let A be Subset of FT;
A1:x in A^b implies ex y1 being Element of FT
st P_1(x,y1,A)=TRUE
proof
assume A2:x in A^b;
reconsider z=x as Element of FT;
U_FT z meets A by A2,FIN_TOPO:13;
then consider w be set such that
A3:w in U_FT z & w in A by XBOOLE_0:3;
reconsider w as Element of FT by A3;
take w;
thus thesis by A3,Def1;
end;
(ex y1 being Element of FT
st P_1(x,y1,A)=TRUE)
implies x in A^b
proof
given y be Element of FT
such that A4:P_1(x,y,A)=TRUE;
(y in U_FT x) & (y in A) by A4,Def1,MARGREL1:38;
then y in (U_FT x /\ A) by XBOOLE_0:def 3;
then U_FT x meets A by XBOOLE_0:def 7;
hence thesis by FIN_TOPO:13;
end;
hence thesis by A1;
end;
definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let A be Subset of FT;
func P_A(x,A) -> Element of BOOLEAN equals
:Def4:
TRUE if x in A
otherwise FALSE;
correctness;
end;
theorem
for x be Element of FT, A be Subset of FT
holds P_A(x,A)=TRUE iff x in A by Def4,MARGREL1:38;
theorem
for x be Element of FT, A be Subset of FT
holds
x in A^deltai iff
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = TRUE
proof
let x be Element of FT;
let A be Subset of FT;
A1: x in A^deltai implies
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = TRUE
proof
assume x in A^deltai;
then x in A /\ (A^delta) by FIN_TOPO:def 7;
then x in A & x in A^delta by XBOOLE_0:def 3;
hence thesis by Def4,Th8;
end;
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = TRUE
implies x in A^deltai
proof
assume (ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = TRUE;
then x in A^delta & x in A by Def4,Th8,MARGREL1:38;
then x in A /\ (A^delta) by XBOOLE_0:def 3;
hence thesis by FIN_TOPO:def 7;
end;
hence thesis by A1;
end;
theorem
for x be Element of FT, A be Subset of FT
holds
x in A^deltao iff
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = FALSE
proof
let x be Element of FT;
let A be Subset of FT;
A1: x in A^deltao implies
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = FALSE
proof
assume x in A^deltao;
then x in A` /\ (A^delta) by FIN_TOPO:def 8;
then x in A` & x in A^delta by XBOOLE_0:def 3;
then not x in A & x in A^delta by SUBSET_1:54;
hence thesis by Def4,Th8;
end;
(ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = FALSE
implies x in A^deltao
proof
assume (ex y1,y2 being Element of FT
st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = FALSE;
then x in A^delta & (x in (the carrier of FT) & not(x in A))
by Def4,Th8,MARGREL1:38;
then x in A^delta & (x in (the carrier of FT) \ A) by XBOOLE_0:def 4;
then x in A^delta & x in A` by SUBSET_1:def 5;
then x in A` /\ (A^delta) by XBOOLE_0:def 3;
hence thesis by FIN_TOPO:def 8;
end;
hence thesis by A1;
end;
definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
func P_e(x,y) -> Element of BOOLEAN equals
:Def5:
TRUE if x = y
otherwise FALSE;
correctness;
end;
theorem
for x,y be Element of FT
holds P_e(x,y)=TRUE iff x = y by Def5,MARGREL1:38;
theorem
for x be Element of FT, A be Subset of FT
holds
x in A^s iff
P_A(x,A)=TRUE &
not(ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE))
proof
let x be Element of FT;
let A be Subset of FT;
A1:x in A^s implies
P_A(x,A)=TRUE &
not(ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE))
proof
assume x in A^s;
then A2: x in A & (U_FT x \ {x}) misses A by FIN_TOPO:14;
then A3:x in A & (U_FT x \ {x}) /\ A = {} by XBOOLE_0:def 7;
not(ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE))
proof
given y being Element of FT
such that A4: P_1(x,y,A)=TRUE and
A5: P_e(x,y)=FALSE;
A6: (y in U_FT x) & (y in A) by A4,Def1,MARGREL1:38;
not x = y by A5,Def5,MARGREL1:38;
then not y in {x} by TARSKI:def 1;
then y in (U_FT x \ {x}) by A6,XBOOLE_0:def 4;
hence contradiction by A3,A6,XBOOLE_0:def 3;
end;
hence thesis by A2,Def4;
end;
(P_A(x,A)=TRUE &
not(ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE)))
implies x in A^s
proof
assume A7:P_A(x,A)=TRUE &
not(ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE));
then A8: x in A by Def4,MARGREL1:38;
for y be Element of FT holds not(y in ((U_FT x \ {x}) /\ A
)
)
proof
let y be Element of FT;
not (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE) by A7;
then not((y in U_FT x) & (not x = y) & (y in A))
by Def1,Def5;
then not((y in U_FT x) & (not y in {x}) & (y in A)) by TARSKI:def 1;
then not(y in (U_FT x \ {x}) & (y in A)) by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then (U_FT x \ {x}) /\ A = {} by SUBSET_1:10;
then (U_FT x \ {x}) misses A by XBOOLE_0:def 7;
hence thesis by A8,FIN_TOPO:14;
end;
hence thesis by A1;
end;
theorem
for x be Element of FT, A be Subset of FT
holds
x in A^n iff
P_A(x,A)=TRUE &
ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE)
proof
let x be Element of FT;
let A be Subset of FT;
A1:x in A^n implies
P_A(x,A)=TRUE &
ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE)
proof
assume x in A^n;
then A2: x in A & (U_FT x \ {x}) meets A by FIN_TOPO:15;
then x in A & (U_FT x \ {x}) /\ A <> {} by XBOOLE_0:def 7;
then consider y being Element of FT
such that A3: y in ((U_FT x \ {x}) /\ A) by SUBSET_1:10;
A4: (y in U_FT x \ {x}) & (y in A) by A3,XBOOLE_0:def 3;
then A5: y in U_FT x & not y in {x} by XBOOLE_0:def 4;
then not x = y by TARSKI:def 1;
then A6: P_e(x,y)=FALSE by Def5;
P_1(x,y,A)=TRUE by A4,A5,Def1;
hence thesis by A2,A6,Def4;
end;
(P_A(x,A)=TRUE &
ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE))
implies x in A^n
proof
assume A7:P_A(x,A)=TRUE &
ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE);
then A8: x in A by Def4,MARGREL1:38;
consider y being Element of FT
such that A9:(P_1(x,y,A)=TRUE & P_e(x,y)=FALSE) by A7;
(y in U_FT x) & (y in A) & (x <> y)
by A9,Def1,Def5,MARGREL1:38;
then (y in U_FT x) & (not y in {x}) & (y in A) by TARSKI:def 1;
then y in (U_FT x \ {x}) & (y in A) by XBOOLE_0:def 4;
then (U_FT x \ {x}) meets A by XBOOLE_0:3;
hence thesis by A8,FIN_TOPO:15;
end;
hence thesis by A1;
end;
theorem
for x be Element of FT, A be Subset of FT
holds
x in A^f iff
(ex y being Element of FT st P_A(y,A)=TRUE & P_0(y,x)=TRUE)
proof
let x be Element of FT;
let A be Subset of FT;
A1: x in A^f implies
(ex y being Element of FT st P_A(y,A)=TRUE & P_0(y,x)=TRUE)
proof
assume x in A^f;
then consider y being Element of FT
such that A2: y in A & x in U_FT y by FIN_TOPO:16;
A3: P_A(y,A)=TRUE by A2,Def4;
P_0(y,x)=TRUE by A2,Def3;
hence thesis by A3;
end;
(ex y being Element of FT st P_A(y,A)=TRUE & P_0(y,x)=TRUE)
implies x in A^f
proof
assume ex y being Element of FT
st P_A(y,A)=TRUE & P_0(y,x)=TRUE;
then consider y being Element of FT
such that A4: P_A(y,A)=TRUE & P_0(y,x)=TRUE;
A5: y in A by A4,Def4,MARGREL1:38;
x in U_FT y by A4,Def3,MARGREL1:38;
hence thesis by A5,FIN_TOPO:16;
end;
hence thesis by A1;
end;
begin
::
:: SECTION2: Formal Topological Spaces
::
definition
struct ( 1-sorted ) FMT_Space_Str
(# carrier -> set,
BNbd -> Function of the carrier, bool bool the carrier #);
end;
definition
cluster non empty strict FMT_Space_Str;
existence
proof consider D being non empty set,f being Function of D, bool bool D;
take FMT_Space_Str(#D,f#);
thus the carrier of FMT_Space_Str(#D,f#) is non empty;
thus thesis;
end;
end;
reserve T for non empty TopStruct;
reserve FMT for non empty FMT_Space_Str;
reserve x, y for Element of FMT;
definition
let FMT;
let x be Element of FMT;
func U_FMT x -> Subset of bool the carrier of FMT equals
:Def6:
( the BNbd of FMT ).x;
correctness;
end;
definition
let T;
func NeighSp T -> non empty strict FMT_Space_Str means
the carrier of it = the carrier of T &
for x being Point of it holds
U_FMT x = {V where V is Subset of T: V in the topology of T & x in V};
existence
proof
ex IT being non empty strict FMT_Space_Str
st the carrier of IT = the carrier of T &
for x being Point of IT holds
U_FMT x = {V where V is Subset of T: V in the topology of T & x in V}
proof
deffunc F(set) =
{V where V is Subset of T: V in the topology of T & $1 in V};
A1:for x being Element of T holds
F(x) in bool bool the carrier of T
proof
let x being Element of T;
now let Y be set;
assume Y in {V where V is Subset of T: V in the topology of T & x in
V};
then consider V being Subset of T such that
A2:V=Y & V in the topology of T & x in V;
thus Y in bool the carrier of T by A2;
end;
then {V where V is Subset of T: V in the topology of T & x in V}
c= bool the carrier of T by TARSKI:def 3;
hence thesis;
end;
consider f be Function of the carrier of T,bool bool the carrier of T
such that A3: for x being Element of T holds
f.x = F(x) from FunctR_ealEx(A1);
reconsider IT = FMT_Space_Str(#the carrier of T,f#)
as non empty strict FMT_Space_Str by STRUCT_0:def 1;
A4: for x being Element of IT holds
U_FMT x
= {V where V is Subset of T: V in the topology of T & x in V}
proof
let x be Element of IT;
thus U_FMT x
= f.x by Def6
.= {V where V is Subset of T: V in the topology of T & x in V} by A3;
end;
take IT;
thus thesis by A4;
end;
hence thesis;
end;
uniqueness
proof
let it1,it2 be non empty strict FMT_Space_Str such that
A5: the carrier of it1 = the carrier of T and
A6: for x being Point of it1 holds
U_FMT x = {V where V is Subset of T: V in the topology of T & x in V}
and
A7: the carrier of it2 = the carrier of T and
A8: for x being Point of it2 holds
U_FMT x = {V where V is Subset of T: V in the topology of T & x in V};
A9:for x being Element of it1 holds
(the BNbd of it1).x
= {V where V is Subset of T: V in the topology of T & x in V}
proof
let x be Element of it1;
(the BNbd of it1).x = U_FMT x by Def6;
hence thesis by A6;
end;
A10:for x being Element of it2 holds
(the BNbd of it2).x
= {V where V is Subset of T: V in the topology of T & x in V}
proof
let x be Element of it2;
(the BNbd of it2).x = U_FMT x by Def6;
hence thesis by A8;
end;
now let x being Point of it1;
thus (the BNbd of it1).x
= {V where V is Subset of T: V in the topology of T & x in V} by A9
.= (the BNbd of it2).x by A5,A7,A10;
end;
hence it1=it2 by A5,A7,FUNCT_2:113;
end;
end;
reserve A, B, W, V for Subset of FMT;
definition let IT be non empty FMT_Space_Str;
attr IT is Fo_filled means
:Def8:
for x being Element of IT
for D being Subset of IT st D in U_FMT x holds x in D;
end;
definition
let FMT;
let A;
func A^Fodelta -> Subset of FMT equals :Def9:
{x:for W st W in U_FMT x holds W meets A & W meets A`};
coherence
proof
defpred P[Element of FMT] means
for W st W in U_FMT $1 holds W meets A & W meets A`;
deffunc F(Element of FMT) = $1;
{F(x): P[x]} is Subset of FMT from SubsetFD;
hence thesis;
end;
end;
canceled;
theorem Th20:
x in A^Fodelta iff for W st W in U_FMT x holds W meets A & W meets A`
proof
thus x in A^Fodelta implies for W st W in U_FMT x holds W meets A &
W meets A`
proof
assume x in A^Fodelta;
then x in {y:for W st W in U_FMT y holds W meets A & W meets A`}
by Def9;
then ex y st y=x & for W st W in U_FMT y holds W meets A &
W meets A`;
hence thesis;
end;
assume for W st W in U_FMT x holds W meets A & W meets A`;
then x in {y:for W st W in U_FMT y holds W meets A & W meets A`};
hence x in A^Fodelta by Def9;
end;
definition
let FMT,A;
func A^Fob -> Subset of FMT equals
:Def10:
{x:for W st W in U_FMT x holds W meets A};
coherence
proof
defpred P[Element of FMT] means
for W st W in U_FMT $1 holds W meets A;
deffunc F(Element of FMT) = $1;
{F(x): P[x]} is Subset of FMT from SubsetFD;
hence thesis;
end;
end;
theorem Th21:
x in A^Fob iff for W st W in U_FMT x holds W meets A
proof
thus x in A^Fob implies for W st W in U_FMT x holds W meets A
proof
assume x in A^Fob;
then x in {y:for W st W in U_FMT y holds W meets A} by Def10;
then ex y st y=x & for W st W in U_FMT y holds W meets A;
hence thesis;
end;
assume for W st W in U_FMT x holds W meets A;
then x in {y:for W st W in U_FMT y holds W meets A};
hence thesis by Def10;
end;
definition
let FMT,A;
func A^Foi -> Subset of FMT equals
:Def11:
{x:ex V st V in U_FMT x & V c= A};
coherence
proof
defpred P[Element of FMT] means
ex V st V in U_FMT $1 & V c= A;
deffunc F(Element of FMT) = $1;
{F(x): P[x]} is Subset of FMT from SubsetFD;
hence thesis;
end;
end;
theorem Th22:
x in A^Foi iff ex V st V in U_FMT x & V c= A
proof
thus x in A^Foi implies ex V st V in U_FMT x & V c= A
proof
assume x in A^Foi;
then x in {y:ex V st V in U_FMT y & V c= A} by Def11;
then ex y st y=x & ex V st V in U_FMT y & V c= A;
hence thesis;
end;
assume ex V st V in U_FMT x & V c= A;
then x in {y:ex V st V in U_FMT y & V c= A};
hence thesis by Def11;
end;
definition
let FMT,A;
func A^Fos -> Subset of FMT equals
:Def12:
{x:x in A & (ex V st V in U_FMT x & V \ {x} misses A)};
coherence
proof
defpred P[Element of FMT] means
$1 in A & (ex V st V in U_FMT $1 & (V \ {$1}) misses A);
deffunc F(Element of FMT) = $1;
{F(x): P[x]} is Subset of FMT from SubsetFD;
hence thesis;
end;
end;
theorem Th23:
x in A^Fos iff x in A & (ex V st V in U_FMT x & V \ {x} misses A)
proof
thus x in A^Fos implies x in A & (ex V st V in U_FMT x & V \ {x} misses A)
proof
assume x in A^Fos;
then x in {y:y in A & (ex V st V in
U_FMT y & (V \ {y}) misses A)} by Def12;
then ex y st y=x & (y in A & (ex V st V in
U_FMT y & (V \ {y}) misses A));
hence thesis;
end;
assume x in A & (ex V st V in U_FMT x & V \ {x} misses A);
then x in {y:y in A & (ex V st V in U_FMT y & (V \ {y}) misses A)};
hence thesis by Def12;
end;
definition
let FMT,A;
func A^Fon -> Subset of FMT equals
:Def13:
A\(A^Fos);
coherence;
end;
theorem
x in A^Fon iff x in A & (for V st V in U_FMT x holds (V \ {x}) meets A)
proof
thus x in A^Fon implies x in A & (for V st V in
U_FMT x holds (V \ {x}) meets A)
proof
assume x in A^Fon;
then x in A\(A^Fos) by Def13;
then x in A & not x in A^Fos by XBOOLE_0:def 4;
hence x in A & (for V st V in U_FMT x holds (V \ {x}) meets A) by Th23;
end;
assume x in A & (for V st V in U_FMT x holds (V \ {x}) meets A);
then x in A & not x in A^Fos by Th23;
then x in A\(A^Fos) by XBOOLE_0:def 4;
hence x in A^Fon by Def13;
end;
theorem Th25:
for FMT being non empty FMT_Space_Str,
A, B being Subset of FMT holds
A c= B implies A^Fob c= B^Fob
proof
let FMT be non empty FMT_Space_Str;
let A, B be Subset of FMT;
assume A1:A c= B;
let x be set;
assume A2:x in A^Fob;
then reconsider y=x as Element of FMT;
for W being Subset of FMT st W in U_FMT y holds W meets B
proof
let W be Subset of FMT;
assume W in U_FMT y;
then W meets A by A2,Th21;
then consider z being set such that
A3: z in W & z in A by XBOOLE_0:3;
thus W /\ B <> {} by A1,A3,XBOOLE_0:def 3;
end;
hence x in B^Fob by Th21;
end;
theorem Th26:
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT holds
A c= B implies A^Foi c= B^Foi
proof
let FMT be non empty FMT_Space_Str;
let A,B be Subset of FMT;
assume A1:A c= B;
let x be set;
assume A2:x in A^Foi;
then reconsider y=x as Element of FMT;
consider V' be Subset of FMT such that
A3:V' in U_FMT y & V' c= A by A2,Th22;
V' in U_FMT y & V' c= B by A1,A3,XBOOLE_1:1;
hence x in B^Foi by Th22;
end;
theorem Th27:
((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob
proof
let x be set;
assume x in ((A^Fob) \/ (B^Fob));
then A1: x in (A^Fob) or x in (B^Fob) by XBOOLE_0:def 2;
A c= A \/ B & B c= B \/ A by XBOOLE_1:7;
then (A^Fob) c= (A \/ B)^Fob & (B^Fob) c= (B \/ A)^Fob by Th25;
hence thesis by A1;
end;
theorem
(A /\ B)^Fob c= (A^Fob) /\ (B^Fob)
proof
let x be set;
assume A1:x in (A /\ B)^Fob;
A /\ B c= A & B /\ A c= B by XBOOLE_1:17;
then (A /\ B)^Fob c= A^Fob & (B /\ A)^Fob c= B^Fob by Th25;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem
((A^Foi) \/ (B^Foi)) c= (A \/ B)^Foi
proof
let x be set;
assume x in ((A^Foi) \/ (B^Foi));
then A1: x in (A^Foi) or x in (B^Foi) by XBOOLE_0:def 2;
A c= A \/ B & B c= B \/ A by XBOOLE_1:7;
then (A^Foi) c= (A \/ B)^Foi & (B^Foi) c= (B \/ A)^Foi by Th26;
hence thesis by A1;
end;
theorem Th30:
(A /\ B)^Foi c= ((A^Foi) /\ (B^Foi))
proof
let x be set;
assume A1:x in (A /\ B)^Foi;
A /\ B c= A & B /\ A c= B by XBOOLE_1:17;
then (A /\ B)^Foi c= A^Foi & (B /\ A)^Foi c= B^Foi by Th26;
hence x in ((A^Foi) /\ (B^Foi)) by A1,XBOOLE_0:def 3;
end;
theorem
for FMT being non empty FMT_Space_Str holds
(for x being Element of FMT,
V1,V2 being Subset of FMT
st ((V1 in U_FMT x) & (V2 in U_FMT x)) holds
ex W being Subset of FMT
st ((W in U_FMT x) & (W c= (V1 /\ V2))))
iff for A,B being Subset of FMT holds
(A \/ B)^Fob = ((A^Fob) \/ (B^Fob))
proof
let FMT be non empty FMT_Space_Str;
A1: (for x being Element of FMT,
V1,V2 being Subset of FMT
st ((V1 in U_FMT x) & (V2 in U_FMT x)) holds
ex W being Subset of FMT
st ((W in U_FMT x) & (W c= (V1 /\ V2))))
implies for A,B being Subset of FMT holds
(A \/ B)^Fob = ((A^Fob) \/ (B^Fob))
proof
assume A2:(for x being Element of FMT,
V1,V2 being Subset of FMT
st ((V1 in U_FMT x) & (V2 in U_FMT x)) holds
ex W being Subset of FMT
st ((W in U_FMT x) & (W c= (V1 /\ V2))));
let A,B be Subset of FMT;
for x be Element of FMT holds x in ((A \/ B)^Fob)
iff x in ((A^Fob) \/ (B^Fob))
proof
let x be Element of FMT;
A3: x in ((A \/ B)^Fob) implies x in ((A^Fob) \/ (B^Fob))
proof
assume A4:x in ((A \/ B)^Fob);
A5: for W1 being Subset of FMT st W1 in U_FMT x
holds W1 meets A or W1 meets B
proof
let W1 being Subset of FMT;
assume W1 in U_FMT x;
then W1 meets (A \/ B) by A4,Th21;
then W1 /\ (A \/ B) <> {} by XBOOLE_0:def 7;
then (W1 /\ A \/ W1 /\ B) <> {} by XBOOLE_1:23;
then W1 /\ A <> {} or W1 /\ B <> {};
hence thesis by XBOOLE_0:def 7;
end;
for V1,V2 being Subset of FMT
st V1 in U_FMT x & V2 in U_FMT x holds
(V1 meets A or V2 meets B)
proof
let V1,V2 be Subset of FMT;
assume V1 in U_FMT x & V2 in U_FMT x;
then consider W being Subset of FMT such that
A6: W in U_FMT x and A7: W c= (V1 /\ V2) by A2;
W meets A or W meets B by A5,A6;
then W /\ A<> {} or W /\ B<> {} by XBOOLE_0:def 7;
then consider z1,z2 being Element of FMT such that
A8:z1 in W /\ A or z2 in W /\ B by SUBSET_1:10;
(V1 /\ V2) c= V1 & (V1 /\ V2)c= V2 by XBOOLE_1:17;
then W c= V1 & W c= V2 by A7,XBOOLE_1:1;
then (W /\ A c= V1 /\ A) & ( W /\ B c= V2 /\ B) by XBOOLE_1:26;
hence V1 meets A or V2 meets B by A8,XBOOLE_0:def 7;
end;
then (for V1 being Subset of FMT
st V1 in U_FMT x holds V1 meets A) or
(for V2 being Subset of FMT st
V2 in U_FMT x holds V2 meets B);
then x in (A^Fob) or x in (B^Fob) by Th21;
hence thesis by XBOOLE_0:def 2;
end;
x in ((A^Fob) \/ (B^Fob)) implies x in ((A \/ B)^Fob)
proof
assume A9:x in ((A^Fob) \/ (B^Fob));
((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob by Th27;
hence thesis by A9;
end;
hence thesis by A3;
end;
hence (A \/ B)^Fob = (A^Fob) \/ (B^Fob) by SUBSET_1:8;
end;
(for A,B being Subset of FMT holds
(A \/ B)^Fob = ((A^Fob) \/ (B^Fob)) )
implies (for x being Element of FMT,
V1,V2 being Subset of FMT
st ((V1 in U_FMT x) & (V2 in U_FMT x)) holds
ex W being Subset of FMT
st ((W in U_FMT x) & (W c= (V1 /\ V2))))
proof
(ex x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x) & (V2 in U_FMT x) &
(for W being Subset of FMT
st W in U_FMT x holds (not(W c= V1 /\ V2)) ) )
implies ( ex A,B being Subset of FMT
st ((A \/ B)^Fob) <> ((A^Fob) \/ (B^Fob)) )
proof
given x0 being Element of FMT,
V1,V2 being Subset of FMT
such that A10:(V1 in U_FMT x0) & (V2 in U_FMT x0)
and A11: (for W being Subset of FMT
st W in U_FMT x0 holds (not(W c= V1 /\ V2)) );
A12:x0 in ((V1)` \/ (V2)`)^Fob
proof
for W being Subset of FMT
st W in U_FMT x0 holds W meets ((V1)` \/ (V2)`)
proof
let W being Subset of FMT;
assume W in U_FMT x0;
then A13: not (W c= V1 /\ V2) by A11;
W /\ (V1 /\ V2)` <> {}
proof
assume W /\ (V1 /\ V2)` = {};
then W \ (V1 /\ V2) = {} by SUBSET_1:32;
hence contradiction by A13,XBOOLE_1:37;
end;
hence W /\ ((V1)` \/ (V2)`) <> {} by SUBSET_1:30;
end;
hence thesis by Th21;
end;
A14:not x0 in ((V1)`)^Fob
proof
assume A15: x0 in ((V1)`)^Fob;
V1 misses (V1)` by SUBSET_1:26;
hence contradiction by A10,A15,Th21;
end;
A16:not (x0 in ((V2)`)^Fob)
proof
assume A17: x0 in ((V2)`)^Fob;
V2 misses (V2)` by SUBSET_1:26;
hence contradiction by A10,A17,Th21;
end;
take V1`,V2`;
thus thesis by A12,A14,A16,XBOOLE_0:def 2;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem
for FMT being non empty FMT_Space_Str holds
(for x being Element of FMT,
V1,V2 being Subset of FMT
st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT
st (W in U_FMT x & W c= V1 /\ V2))
iff for A,B being Subset of FMT holds
(A^Foi) /\ (B^Foi) = (A /\ B)^Foi
proof
let FMT be non empty FMT_Space_Str;
thus (for x being Element of FMT,
V1,V2 being Subset of FMT
st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT
st (W in U_FMT x & W c= V1 /\ V2))
implies for A,B being Subset of FMT holds
(A^Foi) /\ (B^Foi) = (A /\ B)^Foi
proof
assume A1:(for x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x & V2 in U_FMT x) holds
ex W being Subset of FMT
st (W in U_FMT x & W c= V1 /\ V2));
let A,B be Subset of FMT;
thus (A^Foi) /\ (B^Foi) = (A /\ B)^Foi
proof
for x be Element of FMT
holds x in (A^Foi) /\ (B^Foi) iff x in (A /\ B)^Foi
proof
let x be Element of FMT;
A2: x in (A^Foi) /\ (B^Foi) implies x in (A /\ B)^Foi
proof
assume x in (A^Foi) /\ (B^Foi);
then x in A^Foi & x in B^Foi by XBOOLE_0:def 3;
then (ex W1 being Subset of FMT
st W1 in U_FMT x & W1 c= A) &
( ex W2 being Subset of FMT
st W2 in U_FMT x & W2 c= B) by Th22;
then consider W1,W2 being Subset of FMT such that
A3:(W1 in U_FMT x & W2 in U_FMT x ) and A4:(W1 c= A & W2 c= B);
consider W being Subset of FMT
such that A5:W in U_FMT x and A6:W c= W1 /\ W2 by A1,A3;
W1 /\ W2 c= W1 & W1 /\ W2 c= W2 by XBOOLE_1:17;
then W c= W1 & W c= W2 by A6,XBOOLE_1:1;
then W in U_FMT x & W c= A & W c= B by A4,A5,XBOOLE_1:1;
then W in U_FMT x & W c= A /\ B by XBOOLE_1:19;
hence x in (A /\ B)^Foi by Th22;
end;
x in (A /\ B)^Foi implies x in (A^Foi) /\ (B^Foi)
proof
assume A7:x in (A /\ B)^Foi;
(A /\ B)^Foi c= (A^Foi) /\ (B^Foi) by Th30;
hence thesis by A7;
end;
hence thesis by A2;
end;
hence thesis by SUBSET_1:8;
end; thus thesis;
end;
thus (for A,B being Subset of FMT holds
((A^Foi) /\ (B^Foi)) = (A /\ B)^Foi )
implies (for x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x & V2 in U_FMT x) holds
ex W being Subset of FMT
st (W in U_FMT x & W c= V1 /\ V2))
proof
(ex x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x & V2 in U_FMT x) &
(for W being Subset of FMT
st W in U_FMT x holds (not(W c= V1 /\ V2)) ) )
implies ex A,B being Subset of FMT
st ((A^Foi) /\ (B^Foi)) <> (A /\ B)^Foi
proof
given x0 being Element of FMT,
V1,V2 being Subset of FMT
such that A8:V1 in U_FMT x0 & V2 in U_FMT x0
and A9: (for W being Subset of FMT
st W in U_FMT x0 holds (not W c= V1 /\ V2) );
x0 in (V1)^Foi & x0 in (V2)^Foi by A8,Th22;
then A10:not (x0 in ( ((V1)^Foi) /\ (V2^Foi) ) implies
x0 in ((V1 /\ V2)^Foi) ) by A9,Th22,XBOOLE_0:def 3;
take V1,V2;
thus thesis by A10;
end;
hence thesis;
end;
end;
theorem
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT holds
(for x being Element of FMT,
V1,V2 being Subset of FMT
st ((V1 in U_FMT x) & V2 in U_FMT x) holds
ex W being Subset of FMT
st ((W in U_FMT x) & (W c= (V1 /\ V2))))
implies (A \/ B)^Fodelta c= ((A^Fodelta) \/ (B^Fodelta))
proof
let FMT be non empty FMT_Space_Str;
let A,B be Subset of FMT;
assume A1:(for x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x & V2 in U_FMT x) holds
ex W being Subset of FMT
st W in U_FMT x & W c= V1 /\ V2);
for x be Element of FMT holds x in (A \/ B)^Fodelta
implies x in (A^Fodelta) \/ (B^Fodelta)
proof
let x be Element of FMT;
assume A2:x in (A \/ B)^Fodelta;
A3: for W1 being Subset of FMT st W1 in U_FMT x
holds ((W1 meets A & W1 meets A`) or
(W1 meets B & W1 meets B`))
proof
let W1 being Subset of FMT;
assume A4:W1 in U_FMT x;
then W1 meets (A \/ B) by A2,Th20;
then A5:W1 /\ (A \/ B) <> {} by XBOOLE_0:def 7;
W1 meets (A \/ B)` by A2,A4,Th20;
then A6: W1 /\ (A \/ B)` <> {} by XBOOLE_0:def 7;
A7:(W1 /\ A \/ W1 /\ B) <> {} by A5,XBOOLE_1:23;
W1 /\ (A` /\ B`) <> {} by A6,SUBSET_1:29;
then (W1 /\ A`) /\ B` <> {} & (W1 /\ B`) /\ A` <> {} by XBOOLE_1:16;
then A8:(W1 /\ A`) meets B` & (W1 /\ B`) meets A` by XBOOLE_0:def 7;
then consider z1 being set such that
A9:z1 in (W1 /\ A`) /\ B` by XBOOLE_0:4;
consider z2 being set such that
A10:z2 in (W1 /\ B`) /\ A` by A8,XBOOLE_0:4;
(W1 /\ A <> {} & W1 /\ A` <> {}) or
(W1 /\ B <> {} & W1 /\ B` <> {}) by A7,A9,A10;
hence thesis by XBOOLE_0:def 7;
end;
for V1,V2 being Subset of FMT
st V1 in U_FMT x & V2 in U_FMT x holds
(V1 meets A & V1 meets A`) or (V2 meets B & V2 meets B`)
proof
let V1,V2 be Subset of FMT;
assume V1 in U_FMT x & V2 in U_FMT x;
then consider W being Subset of FMT such that
A11: W in U_FMT x and A12: W c= V1 /\ V2 by A1;
V1 /\ V2 c= V1 & V1 /\ V2 c= V2 by XBOOLE_1:17;
then W c= V1 & W c= V2 by A12,XBOOLE_1:1;
then A13:W /\ A c= V1 /\ A & W /\ A` c= V1 /\ A`
& W /\ B c= V2 /\ B & W /\ B` c= V2 /\ B` by XBOOLE_1:26;
(V1 meets A & V1 meets A`) or (V2 meets B & V2 meets B`)
proof
now per cases by A3,A11;
case A14:W meets A & W meets A`;
then consider z1 being set such that
A15: z1 in W /\ A by XBOOLE_0:4;
consider z2 being set such that
A16:z2 in W /\ A` by A14,XBOOLE_0:4;
thus (V1 meets A & V1 meets A`)
or (V2 meets B & V2 meets B`) by A13,A15,A16,XBOOLE_0:4;
case A17:W meets B & W meets B`;
then consider z3 being set
such that A18: z3 in W /\ B by XBOOLE_0:4;
consider z4 being set
such that A19: z4 in W /\ B` by A17,XBOOLE_0:4;
thus (V1 meets A & V1 meets A`)
or (V2 meets B & V2 meets B`) by A13,A18,A19,XBOOLE_0:4;
end;
hence thesis;
end;
hence thesis;
end;
then (for V1 being Subset of FMT
st V1 in U_FMT x holds (V1 meets A & V1 meets A`)) or
(for V2 being Subset of FMT st
V2 in U_FMT x holds (V2 meets B & V2 meets B`));
then x in (A^Fodelta) or x in (B^Fodelta) by Th20;
hence thesis by XBOOLE_0:def 2;
end;
hence thesis by SUBSET_1:7;
end;
theorem
for FMT being non empty FMT_Space_Str st FMT is Fo_filled
holds (for A,B being Subset of FMT holds
(A \/ B)^Fodelta = ((A^Fodelta) \/ (B^Fodelta)))
implies (for x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x & V2 in U_FMT x) holds
ex W being Subset of FMT
st (W in U_FMT x & W c= (V1 /\ V2)))
proof
let FMT be non empty FMT_Space_Str;
assume A1:FMT is Fo_filled;
(for A,B being Subset of FMT holds
(A \/ B)^Fodelta = ((A^Fodelta) \/ (B^Fodelta)) )
implies (for x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x & V2 in U_FMT x) holds
ex W being Subset of FMT
st (W in U_FMT x & W c= V1 /\ V2))
proof
(ex x being Element of FMT,
V1,V2 being Subset of FMT
st (V1 in U_FMT x) & (V2 in U_FMT x) &
(for W being Subset of FMT
st W in U_FMT x holds (not(W c= V1 /\ V2)) ) )
implies ( ex A,B being Subset of FMT
st ((A \/ B)^Fodelta) <> ((A^Fodelta) \/ (B^Fodelta)) )
proof
given x0 being Element of FMT,
V1,V2 being Subset of FMT
such that A2:(V1 in U_FMT x0) & (V2 in U_FMT x0)
and A3: (for W being Subset of FMT
st W in U_FMT x0 holds (not(W c= V1 /\ V2)) );
A4:x0 in ((V1)` \/ (V2)`)^Fodelta
proof
for W being Subset of FMT st W in U_FMT x0
holds W meets ((V1)` \/ (V2)`) & W meets ((V1)` \/ (V2)`)`
proof
let W being Subset of FMT;
assume A5:W in U_FMT x0;
then A6: not W c= V1 /\ V2 by A3;
A7:W meets (V1 /\ V2)`
proof
assume W /\ (V1 /\ V2)` = {};
then W \ (V1 /\ V2) = {} by SUBSET_1:32;
hence contradiction by A6,XBOOLE_1:37;
end;
x0 in V1 & x0 in V2 by A1,A2,Def8;
then A8:x0 in V1 /\ V2 by XBOOLE_0:def 3;
x0 in W by A1,A5,Def8;
then W /\ ((V1 /\ V2)`)` <> {} by A8,XBOOLE_0:def 3;
then W meets ((V1 /\ V2)`)` by XBOOLE_0:def 7;
hence thesis by A7,SUBSET_1:30;
end;
hence thesis by Th20;
end;
A9:not x0 in ((V1)`)^Fodelta
proof
assume x0 in ((V1)`)^Fodelta;
then V1 meets (V1)` by A2,Th20;
hence contradiction by SUBSET_1:26;
end;
A10:not x0 in ((V2)`)^Fodelta
proof
assume x0 in ((V2)`)^Fodelta;
then V2 meets (V2)` by A2,Th20;
hence contradiction by SUBSET_1:26;
end;
take (V1)`,(V2)`;
thus thesis by A4,A9,A10,XBOOLE_0:def 2;
end;
hence thesis;
end;
hence thesis;
end;
theorem
for x be Element of FMT, A being Subset of
FMT
holds x in A^Fos iff x in A & not x in (A\{x})^Fob
proof
let x be Element of FMT;
let A be Subset of FMT;
A1: x in A^Fos implies
x in A & not x in (A\{x})^Fob
proof
assume A2:x in A^Fos;
then consider V' being Subset of FMT
such that A3:V' in U_FMT x & V' \ {x} misses A by Th23;
V' in U_FMT x & V' /\ {x}` misses A by A3,SUBSET_1:32;
then V' /\ {x}` /\ A = {} by XBOOLE_0:def 7;
then V' /\ ({x}`/\ A) = {} by XBOOLE_1:16;
then V' in U_FMT x & V' misses {x}`/\ A by A3,XBOOLE_0:def 7;
then V' in U_FMT x & V' misses A\{x} by SUBSET_1:32;
hence thesis by A2,Th21,Th23;
end;
x in A & not (x in (A\{x})^Fob) implies x in A^Fos
proof
assume that A4:x in A and A5: not x in (A\{x})^Fob;
consider V' being Subset of FMT
such that A6:V' in U_FMT x & V' misses (A\{x}) by A5,Th21;
V' in U_FMT x & V' misses (A /\ {x}`) by A6,SUBSET_1:32;
then V' in U_FMT x & (V' /\ (A /\ {x}`)) = {} by XBOOLE_0:def 7;
then V' in U_FMT x & (V' /\ {x}`)/\ A = {} by XBOOLE_1:16;
then V' in U_FMT x & (V' \ {x}) /\ A = {} by SUBSET_1:32;
then V' in U_FMT x & (V' \ {x}) misses A by XBOOLE_0:def 7;
hence thesis by A4,Th23;
end;
hence thesis by A1;
end;
theorem Th36:
for FMT being non empty FMT_Space_Str holds FMT is Fo_filled
iff for A being Subset of FMT holds A c= A^Fob
proof
let FMT be non empty FMT_Space_Str;
A1: FMT is Fo_filled implies
for A being Subset of FMT holds A c= A^Fob
proof
assume A2:FMT is Fo_filled;
let A being Subset of FMT;
let x be set;
assume A3:x in A;
then reconsider y=x as Element of FMT;
for W being Subset of FMT st W in U_FMT y
holds W meets A
proof
let W be Subset of FMT;
assume W in U_FMT y;
then y in W by A2,Def8;
hence thesis by A3,XBOOLE_0:3;
end;
hence thesis by Th21;
end;
(for A being Subset of FMT holds
A c= A^Fob) implies FMT is Fo_filled
proof
assume A4:for A being Subset of FMT
holds A c= A^Fob;
assume not(FMT is Fo_filled);
then consider y being Element of FMT,
V being Subset of FMT such that
A5: V in U_FMT y and A6: not y in V by Def8;
A7:V misses {y}
proof
assume V meets {y};
then consider z being set
such that A8:z in V & z in {y} by XBOOLE_0:3;
thus contradiction by A6,A8,TARSKI:def 1;
end;
not {y} c= {y}^Fob
proof
assume A9:{y} c= {y}^Fob;
y in {y} by TARSKI:def 1;
hence contradiction by A5,A7,A9,Th21;
end;
hence contradiction by A4;
end;
hence thesis by A1;
end;
theorem Th37:
for FMT being non empty FMT_Space_Str holds FMT is Fo_filled
iff for A being Subset of FMT holds A^Foi c= A
proof
let FMT be non empty FMT_Space_Str;
A1: FMT is Fo_filled implies
for A being Subset of FMT holds A^Foi c= A
proof
assume A2:FMT is Fo_filled;
let A be Subset of FMT;
let x be set;
assume A3:x in A^Foi;
then reconsider y=x as Element of FMT;
consider V be Subset of FMT such that
A4:V in U_FMT y & V c= A by A3,Th22;
y in V & V c= A by A2,A4,Def8;
hence thesis;
end;
(for A being Subset of FMT holds A^Foi c= A)
implies FMT is Fo_filled
proof
assume A5:for A being Subset of FMT
holds A^Foi c= A;
assume not FMT is Fo_filled;
then consider y being Element of FMT,
V being Subset of FMT
such that A6: V in U_FMT y and A7: not y in V by Def8;
y in V^Foi by A6,Th22;
then not V^Foi c= V by A7;
hence contradiction by A5;
end;
hence thesis by A1;
end;
theorem Th38:
((A`)^Fob)` =A^Foi
proof
for x being set holds x in ((A`)^Fob)` iff x in A^Foi
proof
let x be set;
thus x in ((A`)^Fob)` implies x in A^Foi
proof
assume A1:x in ((A`)^Fob)`;
then reconsider y=x as Element of FMT;
not y in (A`)^Fob by A1,SUBSET_1:54;
then consider V be Subset of FMT such that
A2: V in U_FMT y & V misses A` by Th21;
V /\ A` = {} by A2,XBOOLE_0:def 7;
then V in U_FMT y & V \ A = {} by A2,SUBSET_1:32;
then V in U_FMT y & V c= A by XBOOLE_1:37;
hence x in A^Foi by Th22;
end;
assume A3:x in A^Foi;
then reconsider y=x as Element of FMT;
consider V be Subset of FMT such that
A4:V in U_FMT y & V c= A by A3,Th22;
V in U_FMT y & V \ A = {} by A4,XBOOLE_1:37;
then V in U_FMT y & V /\ A` = {} by SUBSET_1:32;
then V in U_FMT y & V misses A` by XBOOLE_0:def 7;
then not y in (A`)^Fob by Th21;
hence x in ((A`)^Fob)`by FIN_TOPO:21;
end;
hence thesis by TARSKI:2;
end;
theorem Th39:
((A`)^Foi)` = A^Fob
proof
for x being set holds x in ((A`)^Foi)` iff x in A^Fob
proof
let x be set;
thus x in ((A`)^Foi)` implies x in A^Fob
proof
assume A1:x in ((A`)^Foi)`;
then reconsider y=x as Element of FMT;
A2:not y in (A`)^Foi by A1,SUBSET_1:54;
for W being Subset of FMT st
W in U_FMT y holds W meets A
proof
let W be Subset of FMT;
assume W in U_FMT y;
then not W c= A` by A2,Th22;
then consider z being set such that
A3:not(z in W implies z in A`) by TARSKI:def 3;
z in W & z in A by A3,FIN_TOPO:21;
hence thesis by XBOOLE_0:3;
end;
hence x in A^Fob by Th21;
end;
assume A4:x in A^Fob;
then reconsider y=x as Element of FMT;
for W being Subset of FMT st
W in U_FMT y holds not W c= A`
proof
let W be Subset of FMT;
assume W in U_FMT y;
then W meets A by A4,Th21;
then consider z being set such that
A5:z in W & z in A by XBOOLE_0:3;
thus thesis by A5,FIN_TOPO:21;
end;
then not y in (A`)^Foi by Th22;
hence x in ((A`)^Foi)` by FIN_TOPO:21;
end;
hence thesis by TARSKI:2;
end;
theorem Th40:
A^Fodelta = (A^Fob) /\ ((A`)^Fob)
proof
for x being Element of FMT holds x in A^Fodelta
iff x in (A^Fob) /\ ((A`)^Fob)
proof
let x be Element of FMT;
thus x in A^Fodelta implies x in (A^Fob) /\ ((A`)^Fob)
proof
assume x in A^Fodelta;
then (for W being Subset of FMT
st W in U_FMT x holds W meets A ) &
(for W being Subset of FMT
st W in U_FMT x holds W meets A`) by Th20;
then x in (A^Fob) & x in((A`)^Fob) by Th21;
hence x in ((A^Fob) /\ ((A`)^Fob)) by XBOOLE_0:def 3;
end;
assume x in ((A^Fob) /\ ((A`)^Fob));
then x in A^Fob & x in (A`)^Fob by XBOOLE_0:def 3;
then for W being Subset of FMT st W in U_FMT x
holds W meets A & W meets A` by Th21;
hence x in A^Fodelta by Th20;
end;
hence thesis by SUBSET_1:8;
end;
theorem
A^Fodelta = (A^Fob) /\ (A^Foi)`
proof
((A`)^Fob)`= A^Foi by Th38;
hence thesis by Th40;
end;
theorem
A^Fodelta = (A`)^Fodelta
proof
A^Fodelta = (((A`)`)^Fob) /\ ((A`)^Fob) by Th40;
hence thesis by Th40;
end;
theorem
A^Fodelta = A^Fob \ A^Foi
proof
for x being set holds x in A^Fodelta iff x in A^Fob \ A^Foi
proof
let x be set;
thus x in A^Fodelta implies x in A^Fob \ A^Foi
proof
assume x in A^Fodelta;
then x in (A^Fob) /\ (((A`)^Fob)`)` by Th40;
then x in ((A^Fob) /\ (A^Foi)`) by Th38;
hence thesis by SUBSET_1:32;
end;
assume x in A^Fob \ A^Foi;
then x in ((A^Fob) /\ ((A^Foi)`)) by SUBSET_1:32;
then x in ((A^Fob) /\ (((A`)^Fob)`)`) by Th38;
hence thesis by Th40;
end;
hence thesis by TARSKI:2;
end;
definition
let FMT;
let A;
func A^Fodel_i -> Subset of FMT equals
:Def14:
A /\ (A^Fodelta);
coherence;
func A^Fodel_o -> Subset of FMT equals
:Def15:
A` /\ (A^Fodelta);
coherence;
end;
theorem
A^Fodelta = (A^Fodel_i) \/ (A^Fodel_o)
proof
for x being set holds x in (A^Fodelta) iff x in (A^Fodel_i) \/ (A^Fodel_o)
proof
let x be set;
A^Fodelta c= (the carrier of FMT);
then A1:A^Fodelta c= [#](the carrier of FMT) by SUBSET_1:def 4;
thus x in A^Fodelta implies x in (A^Fodel_i) \/ (A^Fodel_o)
proof
assume x in A^Fodelta;
then x in [#](the carrier of FMT) /\ (A^Fodelta) by A1,XBOOLE_1:28;
then x in (A \/ A`) /\ (A^Fodelta) by SUBSET_1:25;
then x in (A /\ (A^Fodelta)) \/ (A` /\ (A^Fodelta)) by XBOOLE_1:23;
then x in (A^Fodel_i) \/ (A` /\ (A^Fodelta)) by Def14;
hence x in (A^Fodel_i) \/ (A^Fodel_o) by Def15;
end;
assume x in (A^Fodel_i) \/ (A^Fodel_o);
then x in A /\ (A^Fodelta) \/ (A^Fodel_o) by Def14;
then x in A /\ (A^Fodelta) \/ A` /\ (A^Fodelta) by Def15;
then x in (A \/ A`) /\ (A^Fodelta) by XBOOLE_1:23;
then x in [#](the carrier of FMT) /\ (A^Fodelta) by SUBSET_1:25;
hence x in A^Fodelta by A1,XBOOLE_1:28;
end;
hence thesis by TARSKI:2;
end;
definition let FMT;
let G be Subset of FMT;
attr G is Fo_open means
:Def16:
G = G^Foi;
attr G is Fo_closed means
:Def17:
G = G^Fob;
end;
theorem
A` is Fo_open implies A is Fo_closed
proof
assume A` is Fo_open;
then A1:(A`) = (A`)^Foi by Def16;
(((A`)^Foi)`)` = (A^Fob)` by Th39;
hence thesis by A1,Def17;
end;
theorem
A` is Fo_closed implies A is Fo_open
proof
assume A` is Fo_closed;
then A1:(A`) = (A`)^Fob by Def17;
(A`)^Fob = (((A`)`)^Foi)` by Th39
.= (A^Foi)`;
then A = (A^Foi)`` by A1
.= A^Foi;
hence thesis by Def16;
end;
theorem
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT st FMT is Fo_filled
holds (for x being Element of FMT holds
{x} in U_FMT x )
implies (A /\ B)^Fob = ((A^Fob) /\ (B^Fob))
proof
let FMT be non empty FMT_Space_Str;
let A,B be Subset of FMT;
assume A1:FMT is Fo_filled;
assume A2:for x being Element of FMT holds
{x} in U_FMT x;
A3: for C being Subset of FMT holds C^Fob c= C
proof
let C be Subset of FMT;
for y being Element of FMT holds y in C^Fob implies y in C
proof
let y be Element of FMT;
A4:{y} in U_FMT y by A2;
assume y in C^Fob;
then {y} meets C by A4,Th21;
then consider z being set
such that A5: z in {y} & z in C by XBOOLE_0:3;
thus y in C by A5,TARSKI:def 1;
end;
hence C^Fob c= C by SUBSET_1:7;
end;
for C being Subset of FMT holds C^Fob = C
proof
let C being Subset of FMT;
C c= C^Fob & C^Fob c= C by A1,A3,Th36;
hence thesis by XBOOLE_0:def 10;
end;
then (A /\ B)^Fob = (A /\ B) & (A^Fob) = A & (B^Fob)= B;
hence thesis;
end;
theorem
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT st FMT is Fo_filled
holds (for x being Element of FMT holds
{x} in U_FMT x )
implies (A^Foi) \/ (B^Foi) = (A \/ B)^Foi
proof
let FMT be non empty FMT_Space_Str;
let A,B be Subset of FMT;
assume A1:FMT is Fo_filled;
assume A2:(for x being Element of FMT holds
{x} in U_FMT x );
A3: for C being Subset of FMT holds C c= C^Foi
proof
let C be Subset of FMT;
for y being Element of FMT holds y in C implies y in
C^Foi
proof
let y be Element of FMT;
A4:{y} in U_FMT y by A2;
assume y in C;
then {y} is Subset of C by SUBSET_1:63;
hence y in C^Foi by A4,Th22;
end;
hence C c= C^Foi by SUBSET_1:7;
end;
for C being Subset of FMT holds C = C^Foi
proof
let C being Subset of FMT;
C c= C^Foi & C^Foi c= C by A1,A3,Th37;
hence thesis by XBOOLE_0:def 10;
end;
then (A \/ B)^Foi = (A \/ B) & (A^Foi) = A & (B^Foi)= B;
hence thesis;
end;