:: Formal topological spaces
:: by Gang Liu , Yasushi Fuwa and Masayoshi Eguchi
::
:: Received October 13, 2000
:: Copyright (c) 2000-2018 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, TARSKI, FIN_TOPO, RCOMP_1,
MARGREL1, XBOOLEAN, STRUCT_0, FUNCT_1, ZFMISC_1, PRE_TOPC, SETFAM_1,
FINTOPO2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, FUNCT_1,
FUNCT_2, FIN_TOPO, ORDERS_2, PRE_TOPC, MARGREL1;
constructors DOMAIN_1, MARGREL1, PRE_TOPC, FIN_TOPO, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, FIN_TOPO;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, STRUCT_0, XBOOLE_0;
equalities SUBSET_1, XBOOLEAN, FIN_TOPO;
expansions TARSKI, XBOOLE_0, FIN_TOPO;
theorems TARSKI, SUBSET_1, FIN_TOPO, FUNCT_2, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1, FUNCT_2;
begin
::
:: SECTION1 : Some Useful Theorems on Finite Topological Spaces
::
reserve FT for non empty RelStr;
reserve A for Subset of FT;
theorem
for FT being non empty RelStr, A,B being Subset of FT holds A c= B
implies A^i c= B^i
proof
let FT be non empty RelStr;
let A,B be Subset of FT;
assume
A1: A c= B;
let x be object;
assume
A2: x in A^i;
then reconsider y=x as Element of FT;
A3: U_FT y c= A by A2,FIN_TOPO:7;
for t being Element of FT st t in U_FT y holds t in B
by A3,A1;
then U_FT y c= B;
hence thesis;
end;
theorem Th2:
A^delta = (A^b) /\ ((A^i)`)
proof
for x being object holds x in A^delta iff x in (A^b) /\ ((A^i)`)
proof
let x be object;
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` by A1,FIN_TOPO:5;
then y in ((A`)^b)``;
then
A2: y in ((A^i)`) by FIN_TOPO:17;
U_FT y meets A by A1,FIN_TOPO:5;
then y in (A^b);
hence thesis by A2,XBOOLE_0:def 4;
end;
assume
A3: x in ((A^b) /\ ((A^i)`));
then reconsider y=x as Element of FT;
x in ((A^i)`) by A3,XBOOLE_0:def 4;
then x in ((((A`)^b)`)`) by FIN_TOPO:17;
then
A4: U_FT y meets A` by FIN_TOPO:8;
x in (A^b) by A3,XBOOLE_0:def 4;
then U_FT y meets A by FIN_TOPO:8;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
theorem
A^delta = A^b \ A^i
proof
for x being object holds x in A^delta iff x in A^b \ A^i
proof
let x be object;
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:13;
end;
assume x in A^b \ A^i;
then x in ((A^b) /\ ((A^i)`)) by SUBSET_1:13;
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;
(A`)^i = (((A`)`)^b)` by FIN_TOPO:17
.= (A^b)`;
then A = (A^b)`` by A1
.= A^b;
hence thesis;
end;
theorem
A` is closed implies A is open
proof
assume A` is closed;
then
A1: (A`) = (A`)^b;
(A`)^b = (((A`)`)^i)` by FIN_TOPO:16
.= (A^i)`;
then A = (A^i)`` by A1
.= A^i;
hence thesis;
end;
definition
let FT be non empty RelStr;
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 RelStr;
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;
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;
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
reconsider z=x as Element of FT;
assume
A2: x in A^delta;
then U_FT z meets A by FIN_TOPO:5;
then consider w1 be object such that
A3: w1 in U_FT z and
A4: w1 in A by XBOOLE_0:3;
reconsider w1 as Element of FT by A3;
take w1;
U_FT z meets A` by A2,FIN_TOPO:5;
then consider w2 be object such that
A5: w2 in U_FT z & w2 in A` by XBOOLE_0:3;
take w2;
thus thesis by A3,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;
then U_FT x /\ A <> {} by XBOOLE_0:def 4;
then
A8: U_FT x meets A;
y2 in U_FT x & y2 in A` by A7,Def2;
then U_FT x meets A` by XBOOLE_0:3;
hence thesis by A8;
end;
hence thesis by A1;
end;
definition
let FT be non empty RelStr;
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;
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: (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
A2: 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 A2;
hence thesis by Def1;
end;
then for y be Element of FT holds y in (U_FT x) implies y in A;
then (U_FT x) c= A;
hence thesis;
end;
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 x in A^i;
then
A3: U_FT x c= A by FIN_TOPO:7;
let y be Element of FT;
assume P_0(x,y)=TRUE;
then y in U_FT x by Def3;
hence thesis by A3,Def1;
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
reconsider z=x as Element of FT;
assume x in A^b;
then U_FT z meets A by FIN_TOPO:8;
then consider w be object such that
A2: w in U_FT z and
A3: w in A by XBOOLE_0:3;
reconsider w as Element of FT by A2;
take w;
thus thesis by A2,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;
then y in (U_FT x /\ A) by XBOOLE_0:def 4;
then U_FT x meets A;
hence thesis;
end;
hence thesis by A1;
end;
definition
let FT be non empty RelStr;
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;
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: (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;
hence thesis by XBOOLE_0:def 4;
end;
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 & x in A^delta by XBOOLE_0:def 4;
hence thesis by Def4,Th8;
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: (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 that
A2: ex y1,y2 being Element of FT st P_1(x,y1,A)=TRUE & P_2(x,y2,A)= TRUE and
A3: P_A(x,A) = FALSE;
not x in A by A3,Def4;
then
A4: x in A` by XBOOLE_0:def 5;
x in A^delta by A2,Th8;
hence thesis by A4,XBOOLE_0:def 4;
end;
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
A5: x in A^deltao;
then x in A` by XBOOLE_0:def 4;
then
A6: not x in A by XBOOLE_0:def 5;
x in A^delta by A5,XBOOLE_0:def 4;
hence thesis by A6,Def4,Th8;
end;
hence thesis by A1;
end;
definition
let FT be non empty RelStr;
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;
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
A2: x in A^s;
then (U_FT x \ {x}) misses A by FIN_TOPO:9;
then
A3: (U_FT x \ {x}) /\ A = {};
A4: 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
A5: P_1(x,y,A)=TRUE and
A6: P_e(x,y)=FALSE;
not x = y by A6,Def5;
then
A7: not y in {x} by TARSKI:def 1;
y in U_FT x by A5,Def1;
then
A8: y in (U_FT x \ {x}) by A7,XBOOLE_0:def 5;
y in A by A5,Def1;
hence contradiction by A3,A8,XBOOLE_0:def 4;
end;
x in A by A2,FIN_TOPO:9;
hence thesis by A4,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 that
A9: P_A(x,A)=TRUE and
A10: not(ex y being Element of FT st P_1(x,y,A)=TRUE & P_e(x,y)=FALSE );
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 A10;
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 5;
hence thesis by XBOOLE_0:def 4;
end;
then (U_FT x \ {x}) /\ A = {} by SUBSET_1:4;
then
A11: (U_FT x \ {x}) misses A;
x in A by A9,Def4;
hence thesis by A11;
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
A2: x in A^n;
then (U_FT x \ {x}) meets A by FIN_TOPO:10;
then (U_FT x \ {x}) /\ A <> {};
then consider y being Element of FT such that
A3: y in ((U_FT x \ {x}) /\ A) by SUBSET_1:4;
A4: y in U_FT x \ {x} by A3,XBOOLE_0:def 4;
then
A5: y in U_FT x by XBOOLE_0:def 5;
not y in {x} by A4,XBOOLE_0:def 5;
then not x = y by TARSKI:def 1;
then
A6: P_e(x,y)=FALSE by Def5;
y in A by A3,XBOOLE_0:def 4;
then
A7: P_1(x,y,A)=TRUE by A5,Def1;
x in A by A2,FIN_TOPO:10;
hence thesis by A6,A7,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 that
A8: P_A(x,A)=TRUE and
A9: ex y being Element of FT st P_1(x,y,A)=TRUE & P_e(x,y)=FALSE;
consider y being Element of FT such that
A10: P_1(x,y,A)=TRUE and
A11: P_e(x,y)=FALSE by A9;
x <> y by A11,Def5;
then
A12: not y in {x} by TARSKI:def 1;
y in U_FT x by A10,Def1;
then
A13: y in (U_FT x \ {x}) by A12,XBOOLE_0:def 5;
y in A by A10,Def1;
then
A14: (U_FT x \ {x}) meets A by A13,XBOOLE_0:3;
x in A by A8,Def4;
hence thesis by A14,FIN_TOPO:10;
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: (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
A2: P_A(y,A)=TRUE & P_0(y,x)=TRUE;
y in A & x in U_FT y by A2,Def3,Def4;
hence thesis;
end;
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
A3: y in A & x in U_FT y by FIN_TOPO:11;
P_A(y,A)=TRUE & P_0(y,x)=TRUE by A3,Def3,Def4;
hence thesis;
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;
registration
cluster non empty strict for FMT_Space_Str;
existence
proof
set D = the non empty set,f = the 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-Family of FMT equals
( 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 object;
assume
Y in {V where V is Subset of T: V in the topology of T & x in V};
then ex V being Subset of T st V=Y & V in the topology of T & x in V;
hence Y in bool the carrier of T;
end;
then {V where V is Subset of T: V in the topology of T & x in V} c=
bool the carrier of T;
hence thesis;
end;
consider f be Function of the carrier of T,bool bool the carrier of T
such that
A2: for x being Element of T holds f.x = F(x) from FUNCT_2:sch 8(A1);
reconsider IT = FMT_Space_Str(#the carrier of T,f#) as non empty strict
FMT_Space_Str;
take IT;
thus thesis by A2;
end;
hence thesis;
end;
uniqueness
proof
let it1,it2 be non empty strict FMT_Space_Str such that
A3: the carrier of it1 = the carrier of T and
A4: 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
A5: the carrier of it2 = the carrier of T and
A6: 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};
A7: 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;
hence thesis by A6;
end;
A8: 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;
hence thesis by A4;
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 A8
.= (the BNbd of it2).x by A3,A5,A7;
end;
hence thesis by A3,A5,FUNCT_2:63;
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
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
{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`;
{ x: P[x]} is Subset of FMT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th19:
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 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`;
hence thesis;
end;
definition
let FMT,A;
func A^Fob -> Subset of FMT equals
{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;
{ x: P[x]} is Subset of FMT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th20:
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 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;
hence thesis;
end;
definition
let FMT,A;
func A^Foi -> Subset of FMT equals
{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;
{x: P[x]} is Subset of FMT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th21:
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 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;
hence thesis;
end;
definition
let FMT,A;
func A^Fos -> Subset of FMT equals
{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);
{x: P[x]} is Subset of FMT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th22:
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 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;
hence thesis;
end;
definition
let FMT,A;
func A^Fon -> Subset of FMT equals
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 & not x in A^Fos by XBOOLE_0:def 5;
hence thesis;
end;
assume that
A1: x in A and
A2: for V st V in U_FMT x holds (V \ {x}) meets A;
not x in A^Fos by A2,Th22;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem Th24:
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 object;
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,Th20;
then ex z being object st z in W & z in A by XBOOLE_0:3;
hence W /\ B <> {} by A1,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem Th25:
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 object;
assume
A2: x in A^Foi;
then reconsider y=x as Element of FMT;
consider V9 be Subset of FMT such that
A3: V9 in U_FMT y and
A4: V9 c= A by A2,Th21;
V9 c= B by A1,A4;
hence thesis by A3;
end;
theorem Th26:
((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob
proof
let x be object;
assume x in ((A^Fob) \/ (B^Fob));
then
A1: x in (A^Fob) or x in (B^Fob) by XBOOLE_0:def 3;
(A^Fob) c= (A \/ B)^Fob & (B^Fob) c= (B \/ A)^Fob by Th24,XBOOLE_1:7;
hence thesis by A1;
end;
theorem
(A /\ B)^Fob c= (A^Fob) /\ (B^Fob)
proof
let x be object;
assume
A1: x in (A /\ B)^Fob;
(A /\ B)^Fob c= A^Fob & (B /\ A)^Fob c= B^Fob by Th24,XBOOLE_1:17;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
((A^Foi) \/ (B^Foi)) c= (A \/ B)^Foi
proof
let x be object;
assume x in ((A^Foi) \/ (B^Foi));
then
A1: x in (A^Foi) or x in (B^Foi) by XBOOLE_0:def 3;
(A^Foi) c= (A \/ B)^Foi & (B^Foi) c= (B \/ A)^Foi by Th25,XBOOLE_1:7;
hence thesis by A1;
end;
theorem Th29:
(A /\ B)^Foi c= ((A^Foi) /\ (B^Foi))
proof
let x be object;
assume
A1: x in (A /\ B)^Foi;
(A /\ B)^Foi c= A^Foi & (B /\ A)^Foi c= B^Foi by Th25,XBOOLE_1:17;
hence thesis by A1,XBOOLE_0:def 4;
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,Th20;
then W1 /\ (A \/ B) <> {};
then (W1 /\ A \/ W1 /\ B) <> {} by XBOOLE_1:23;
then W1 /\ A <> {} or W1 /\ B <> {};
hence thesis;
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;
(V1 /\ V2) c= V1 by XBOOLE_1:17;
then W c= V1 by A7;
then
A8: W /\ A c= V1 /\ A by XBOOLE_1:26;
(V1 /\ V2)c= V2 by XBOOLE_1:17;
then W c= V2 by A7;
then
A9: W /\ B c= V2 /\ B by XBOOLE_1:26;
W meets A or W meets B by A5,A6;
then W /\ A<> {} or W /\ B<> {};
then
ex z1,z2 being Element of FMT st ( z1 in W /\ A or z2 in W /\ B)
by SUBSET_1:4;
hence thesis by A8,A9;
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);
hence thesis by XBOOLE_0:def 3;
end;
x in ((A^Fob) \/ (B^Fob)) implies x in ((A \/ B)^Fob)
proof
assume
A10: x in ((A^Fob) \/ (B^Fob));
((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob by Th26;
hence thesis by A10;
end;
hence thesis by A3;
end;
hence thesis by SUBSET_1:3;
end;
(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
A11: V1 in U_FMT x0 and
A12: V2 in U_FMT x0 and
A13: for W being Subset of FMT st W in U_FMT x0 holds not W c= V1 /\ V2;
A14: not x0 in ((V2)`)^Fob
proof
A15: V2 misses (V2)` by XBOOLE_1:79;
assume x0 in ((V2)`)^Fob;
hence contradiction by A12,A15,Th20;
end;
take V1`,V2`;
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
A16: not W c= V1 /\ V2 by A13;
W /\ (V1 /\ V2)` <> {}
proof
assume W /\ (V1 /\ V2)` = {};
then W \ (V1 /\ V2) = {} by SUBSET_1:13;
hence contradiction by A16,XBOOLE_1:37;
end;
hence W /\ ((V1)` \/ (V2)`) <> {} by XBOOLE_1:54;
end;
then
A17: x0 in ((V1)` \/ (V2)`)^Fob;
not x0 in ((V1)`)^Fob
proof
A18: V1 misses (V1)` by XBOOLE_1:79;
assume x0 in ((V1)`)^Fob;
hence contradiction by A11,A18,Th20;
end;
hence thesis by A17,A14,XBOOLE_0:def 3;
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;
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
A3: x in (A^Foi) /\ (B^Foi);
then x in B^Foi by XBOOLE_0:def 4;
then
A4: ex W2 being Subset of FMT st W2 in U_FMT x & W2 c= B by Th21;
x in A^Foi by A3,XBOOLE_0:def 4;
then ex W1 being Subset of FMT st W1 in U_FMT x & W1 c= A by Th21;
then consider W1,W2 being Subset of FMT such that
A5: W1 in U_FMT x & W2 in U_FMT x and
A6: W1 c= A and
A7: W2 c= B by A4;
consider W being Subset of FMT such that
A8: W in U_FMT x and
A9: W c= W1 /\ W2 by A1,A5;
W1 /\ W2 c= W2 by XBOOLE_1:17;
then W c= W2 by A9;
then
A10: W c= B by A7;
W1 /\ W2 c= W1 by XBOOLE_1:17;
then W c= W1 by A9;
then W c= A by A6;
then W c= A /\ B by A10,XBOOLE_1:19;
hence thesis by A8;
end;
x in (A /\ B)^Foi implies x in (A^Foi) /\ (B^Foi)
proof
assume
A11: x in (A /\ B)^Foi;
(A /\ B)^Foi c= (A^Foi) /\ (B^Foi) by Th29;
hence thesis by A11;
end;
hence thesis by A2;
end;
hence (A^Foi) /\ (B^Foi) = (A /\ B)^Foi by SUBSET_1:3;
end;
(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
A12: V1 in U_FMT x0 & V2 in U_FMT x0 and
A13: for W being Subset of FMT st W in U_FMT x0 holds not W c= V1 /\ V2;
take V1,V2;
x0 in (V1)^Foi & x0 in (V2)^Foi by A12;
then x0 in ( ((V1)^Foi) /\ (V2^Foi) ) by XBOOLE_0:def 4;
hence thesis by A13,Th21;
end;
hence
(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;
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,Th19;
then W1 /\ (A \/ B)` <> {};
then
A5: W1 /\ (A` /\ B`) <> {} by XBOOLE_1:53;
then (W1 /\ A`) /\ B` <> {} by XBOOLE_1:16;
then (W1 /\ A`) meets B`;
then
A6: ex z1 being object st z1 in (W1 /\ A`) /\ B` by XBOOLE_0:4;
(W1 /\ B`) /\ A` <> {} by A5,XBOOLE_1:16;
then (W1 /\ B`) meets A`;
then
A7: ex z2 being object st z2 in (W1 /\ B`) /\ A` by XBOOLE_0:4;
W1 meets (A \/ B) by A2,A4,Th19;
then W1 /\ (A \/ B) <> {};
then (W1 /\ A \/ W1 /\ B) <> {} by XBOOLE_1:23;
then
W1 /\ A <> {} & W1 /\ A` <> {} or W1 /\ B <> {} & W1 /\ B` <> {} by A6,A7
;
hence thesis;
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
A8: W in U_FMT x and
A9: W c= V1 /\ V2 by A1;
V1 /\ V2 c= V2 by XBOOLE_1:17;
then W c= V2 by A9;
then
A10: W /\ B c= V2 /\ B & W /\ B` c= V2 /\ B` by XBOOLE_1:26;
V1 /\ V2 c= V1 by XBOOLE_1:17;
then W c= V1 by A9;
then
A11: W /\ A c= V1 /\ A & W /\ A` c= V1 /\ A` by XBOOLE_1:26;
V1 meets A & V1 meets A` or V2 meets B & V2 meets B`
proof
now
per cases by A3,A8;
case
W meets A & W meets A`;
then (ex z1 being object st z1 in W /\ A )&
ex z2 being object st z2 in
W /\ A` by XBOOLE_0:4;
hence thesis by A11;
end;
case
W meets B & W meets B`;
then (ex z3 being object st z3 in W /\ B )&
ex z4 being object st z4 in
W /\ B` by XBOOLE_0:4;
hence thesis by A10;
end;
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);
hence thesis by XBOOLE_0:def 3;
end;
hence thesis;
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;
(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 and
A3: V2 in U_FMT x0 and
A4: for W being Subset of FMT st W in U_FMT x0 holds not W c= V1 /\ V2;
take (V1)`,(V2)`;
A5: not x0 in ((V2)`)^Fodelta
proof
assume x0 in ((V2)`)^Fodelta;
then V2 meets (V2)` by A3,Th19;
hence contradiction by XBOOLE_1:79;
end;
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
A6: W in U_FMT x0;
then
A7: not W c= V1 /\ V2 by A4;
A8: W meets (V1 /\ V2)`
proof
assume W /\ (V1 /\ V2)` = {};
then W \ (V1 /\ V2) = {} by SUBSET_1:13;
hence contradiction by A7,XBOOLE_1:37;
end;
x0 in V1 & x0 in V2 by A1,A2,A3;
then
A9: x0 in V1 /\ V2 by XBOOLE_0:def 4;
x0 in W by A1,A6;
then W /\ ((V1 /\ V2)`)` <> {} by A9,XBOOLE_0:def 4;
then W meets ((V1 /\ V2)`)`;
hence thesis by A8,XBOOLE_1:54;
end;
then
A10: x0 in ((V1)` \/ (V2)`)^Fodelta;
not x0 in ((V1)`)^Fodelta
proof
assume x0 in ((V1)`)^Fodelta;
then V1 meets (V1)` by A2,Th19;
hence contradiction by XBOOLE_1:79;
end;
hence thesis by A10,A5,XBOOLE_0:def 3;
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 & not x in (A\{x})^Fob implies x in A^Fos
proof
assume that
A2: x in A and
A3: not x in (A\{x})^Fob;
consider V9 being Subset of FMT such that
A4: V9 in U_FMT x and
A5: V9 misses (A\{x}) by A3;
V9 misses (A /\ {x}`) by A5,SUBSET_1:13;
then (V9 /\ (A /\ {x}`)) = {};
then (V9 /\ {x}`)/\ A = {} by XBOOLE_1:16;
then (V9 \ {x}) /\ A = {} by SUBSET_1:13;
then (V9 \ {x}) misses A;
hence thesis by A2,A4;
end;
x in A^Fos implies x in A & not x in (A\{x})^Fob
proof
assume
A6: x in A^Fos;
then consider V9 being Subset of FMT such that
A7: V9 in U_FMT x and
A8: V9 \ {x} misses A by Th22;
V9 /\ {x}` misses A by A8,SUBSET_1:13;
then V9 /\ {x}` /\ A = {};
then V9 /\ ({x}`/\ A) = {} by XBOOLE_1:16;
then V9 misses {x}`/\ A;
then V9 misses A\{x} by SUBSET_1:13;
hence thesis by A6,A7,Th20,Th22;
end;
hence thesis by A1;
end;
theorem Th35:
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: (for A being Subset of FMT holds A c= A^Fob) implies FMT is Fo_filled
proof
assume
A2: 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
A3: V in U_FMT y and
A4: not y in V;
A5: V misses {y}
proof
assume V meets {y};
then ex z being object st z in V & z in {y} by XBOOLE_0:3;
hence contradiction by A4,TARSKI:def 1;
end;
not {y} c= {y}^Fob
proof
A6: y in {y} by TARSKI:def 1;
assume {y} c= {y}^Fob;
hence contradiction by A3,A5,A6,Th20;
end;
hence contradiction by A2;
end;
FMT is Fo_filled implies for A being Subset of FMT holds A c= A^Fob
proof
assume
A7: FMT is Fo_filled;
let A being Subset of FMT;
let x be object;
assume
A8: 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 A7;
hence thesis by A8,XBOOLE_0:3;
end;
hence thesis;
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^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 object;
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 and
A5: V c= A by A3,Th21;
y in V by A2,A4;
hence thesis by A5;
end;
(for A being Subset of FMT holds A^Foi c= A) implies FMT is Fo_filled
proof
assume
A6: 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
A7: V in U_FMT y and
A8: not y in V;
y in V^Foi by A7;
then not V^Foi c= V by A8;
hence contradiction by A6;
end;
hence thesis by A1;
end;
theorem Th37:
((A`)^Fob)` =A^Foi
proof
for x being object holds x in ((A`)^Fob)` iff x in A^Foi
proof
let x be object;
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,XBOOLE_0:def 5;
then consider V be Subset of FMT such that
A2: V in U_FMT y and
A3: V misses A`;
V /\ A` = {} by A3;
then V \ A = {} by SUBSET_1:13;
then V c= A by XBOOLE_1:37;
hence thesis by A2;
end;
assume
A4: x in A^Foi;
then reconsider y=x as Element of FMT;
consider V be Subset of FMT such that
A5: V in U_FMT y and
A6: V c= A by A4,Th21;
V \ A = {} by A6,XBOOLE_1:37;
then V /\ A` = {} by SUBSET_1:13;
then V misses A`;
then not y in (A`)^Fob by A5,Th20;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem Th38:
((A`)^Foi)` = A^Fob
proof
for x being object holds x in ((A`)^Foi)` iff x in A^Fob
proof
let x be object;
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,XBOOLE_0:def 5;
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;
then consider z being object such that
A3: z in W and
A4: not z in A`;
z in A by A3,A4,XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:3;
end;
hence thesis;
end;
assume
A5: 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 A5,Th20;
then ex z being object st z in W & z in A by XBOOLE_0:3;
hence thesis by XBOOLE_0:def 5;
end;
then not y in (A`)^Foi by Th21;
hence thesis by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem Th39:
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
A1: x in A^Fodelta;
then for W being Subset of FMT st W in U_FMT x holds W meets A` by Th19;
then
A2: x in((A`)^Fob);
for W being Subset of FMT st W in U_FMT x holds W meets A by A1,Th19;
then x in (A^Fob);
hence thesis by A2,XBOOLE_0:def 4;
end;
assume x in ((A^Fob) /\ ((A`)^Fob));
then x in A^Fob & x in (A`)^Fob by XBOOLE_0:def 4;
then
for W being Subset of FMT st W in U_FMT x holds W meets A & W meets A`
by Th20;
hence thesis;
end;
hence thesis by SUBSET_1:3;
end;
theorem
A^Fodelta = (A^Fob) /\ (A^Foi)`
proof
((A`)^Fob)`= A^Foi by Th37;
hence thesis by Th39;
end;
theorem
A^Fodelta = (A`)^Fodelta
proof
A^Fodelta = (((A`)`)^Fob) /\ ((A`)^Fob) by Th39;
hence thesis by Th39;
end;
theorem
A^Fodelta = A^Fob \ A^Foi
proof
for x being object holds x in A^Fodelta iff x in A^Fob \ A^Foi
proof
let x be object;
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 Th39;
then x in ((A^Fob) /\ (A^Foi)`) by Th37;
hence thesis by SUBSET_1:13;
end;
assume x in A^Fob \ A^Foi;
then x in ((A^Fob) /\ ((A^Foi)`)) by SUBSET_1:13;
then x in ((A^Fob) /\ (((A`)^Fob)`)`) by Th37;
hence thesis by Th39;
end;
hence thesis by TARSKI:2;
end;
definition
let FMT;
let A;
func A^Fodel_i -> Subset of FMT equals
A /\ (A^Fodelta);
coherence;
func A^Fodel_o -> Subset of FMT equals
A` /\ (A^Fodelta);
coherence;
end;
theorem
A^Fodelta = (A^Fodel_i) \/ (A^Fodel_o)
proof
for x being object
holds x in (A^Fodelta) iff x in (A^Fodel_i) \/ (A ^Fodel_o )
proof
let x be object;
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 XBOOLE_1:28;
then x in (A \/ A`) /\ (A^Fodelta) by SUBSET_1:10;
hence thesis by XBOOLE_1:23;
end;
assume x in (A^Fodel_i) \/ (A^Fodel_o);
then x in (A \/ A`) /\ (A^Fodelta) by XBOOLE_1:23;
then x in [#](the carrier of FMT) /\ (A^Fodelta) by SUBSET_1:10;
hence thesis by 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
G = G^Foi;
attr G is Fo_closed means
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;
(((A`)^Foi)`)` = (A^Fob)` by Th38;
hence thesis by A1;
end;
theorem
A` is Fo_closed implies A is Fo_open
proof
assume A` is Fo_closed;
then
A1: (A`) = (A`)^Fob;
(A`)^Fob = (((A`)`)^Foi)` by Th38
.= (A^Foi)`;
then A = (A^Foi)`` by A1
.= A^Foi;
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 /\ 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;
assume
A4: y in C^Fob;
{y} in U_FMT y by A2;
then {y} meets C by A4,Th20;
then ex z being object st z in {y} & z in C by XBOOLE_0:3;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
A5: for C being Subset of FMT holds C^Fob = C
by A1,A3,Th35;
then (A /\ B)^Fob = (A /\ B) & (A^Fob) = A;
hence thesis by A5;
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;
assume y in C;
then
A4: {y} is Subset of C by SUBSET_1:41;
{y} in U_FMT y by A2;
hence thesis by A4;
end;
hence thesis;
end;
A5: for C being Subset of FMT holds C = C^Foi
by A1,A3,Th36;
then (A \/ B)^Foi = (A \/ B) & (A^Foi) = A;
hence thesis by A5;
end;