:: Subsets of Topological Spaces
:: by Miros{\l}aw Wysocki and Agata Darmochwa\l
::
:: Received April 28, 1989
:: Copyright (c) 1990-2016 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 STRUCT_0, SUBSET_1, PRE_TOPC, XBOOLE_0, RCOMP_1, TARSKI, TOPS_1;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
constructors SETFAM_1, PRE_TOPC;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;
theorems PRE_TOPC, TARSKI, SUBSET_1, XBOOLE_0, XBOOLE_1;
begin
reserve TS for 1-sorted,
K, Q for Subset of TS;
theorem
K` = Q` implies K = Q by SUBSET_1:42;
::
:: CLOSED AND OPEN SETS, CLOSURE OF SET
::
reserve TS for TopSpace,
GX for TopStruct,
x for set,
P, Q for Subset of TS,
K , L for Subset of TS,
R, S for Subset of GX,
T, W for Subset of GX;
theorem Th2:
Cl([#] GX) = [#] GX
by PRE_TOPC:18;
registration
let T be TopSpace, P be Subset of T;
cluster Cl P -> closed;
coherence
proof
Cl Cl P = Cl P;
hence thesis by PRE_TOPC:22;
end;
end;
theorem Th3:
R is closed iff R` is open
proof
R is closed iff [#] GX \ R is open by PRE_TOPC:def 3;
hence thesis;
end;
registration
let T be TopSpace, R be closed Subset of T;
cluster R` -> open;
coherence by Th3;
end;
theorem Th4:
R is open iff R` is closed
proof
R` is closed iff R`` is open by Th3;
hence thesis;
end;
registration
let T be TopSpace;
cluster open for Subset of T;
existence
proof
take ({}T)`;
thus thesis;
end;
end;
registration
let T be TopSpace, R be open Subset of T;
cluster R` -> closed;
coherence by Th4;
end;
theorem
S is closed & T c= S implies Cl T c= S
proof
assume that
A1: S is closed and
A2: T c= S;
Cl S = S by A1,PRE_TOPC:22;
hence thesis by A2,PRE_TOPC:19;
end;
theorem Th6:
Cl K \ Cl L c= Cl(K \ L)
proof
let x be object;
Cl K \/ Cl L = Cl (K \/ L) by PRE_TOPC:20
.= Cl((K \ L) \/ L) by XBOOLE_1:39
.= Cl(K \ L) \/ Cl L by PRE_TOPC:20;
then
A1: x in Cl K \/ Cl L iff x in Cl(K \ L) or x in Cl L by XBOOLE_0:def 3;
assume
A2: x in (Cl K \ Cl L);
then x in Cl K by XBOOLE_0:def 5;
hence thesis by A2,A1,XBOOLE_0:def 3,def 5;
end;
theorem Th7:
R is closed & S is closed implies Cl(R /\ S) = Cl R /\ Cl S
proof
assume that
A1: R is closed and
A2: S is closed;
A3: S = Cl S by A2,PRE_TOPC:22;
A4: Cl(R /\ S) c= Cl R /\ Cl S by PRE_TOPC:21;
R = Cl R by A1,PRE_TOPC:22;
then Cl R /\ Cl S c= Cl(R /\ S) by A3,PRE_TOPC:18;
hence thesis by A4;
end;
registration
let TS;
let P,Q be closed Subset of TS;
cluster P /\ Q -> closed for Subset of TS;
coherence
proof
A1: Q = Cl Q by PRE_TOPC:22;
P = Cl P by PRE_TOPC:22;
then Cl(P /\ Q) = P /\ Q by A1,Th7;
hence thesis;
end;
cluster P \/ Q -> closed for Subset of TS;
coherence
proof
A2: Q = Cl Q by PRE_TOPC:22;
P = Cl P by PRE_TOPC:22;
then Cl(P \/ Q) = P \/ Q by A2,PRE_TOPC:20;
hence thesis;
end;
end;
theorem
P is closed & Q is closed implies P /\ Q is closed;
theorem
P is closed & Q is closed implies P \/ Q is closed;
registration
let TS;
let P,Q be open Subset of TS;
cluster P /\ Q -> open for Subset of TS;
coherence
proof
(P`) \/ Q` = (P /\ Q)` by XBOOLE_1:54;
hence thesis by Th4;
end;
cluster P \/ Q -> open for Subset of TS;
coherence
proof
(P`) /\ Q` = (P \/ Q)` by XBOOLE_1:53;
hence thesis by Th4;
end;
end;
theorem
P is open & Q is open implies P \/ Q is open;
theorem
P is open & Q is open implies P /\ Q is open;
theorem Th12:
for GX being non empty TopSpace, R being Subset of GX, p being
Point of GX holds p in Cl R iff for T being Subset of GX st T is open & p in T
holds R meets T
proof
let GX be non empty TopSpace, R be Subset of GX, p be Point of GX;
hereby
assume
A1: p in Cl R;
given T being Subset of GX such that
A2: T is open and
A3: p in T and
A4: R misses T;
A5: (R`) \/ T` = (R /\ T)` by XBOOLE_1:54;
A6: R /\ T = {} GX by A4;
A7: R c= T`
proof
let x be object;
assume
A8: x in R;
then x in R` or x in T` by A5,A6,XBOOLE_0:def 3;
hence thesis by A8,XBOOLE_0:def 5;
end;
Cl(T`) = T` by A2,PRE_TOPC:22;
then Cl R c= T` by A7,PRE_TOPC:19;
hence contradiction by A1,A3,XBOOLE_0:def 5;
end;
assume
A9: for T being Subset of GX st T is open & p in T holds R meets T;
assume not p in Cl R;
then p in (Cl R)` by SUBSET_1:29;
then
A10: R meets (Cl R)` by A9;
R misses R` by XBOOLE_1:79;
then
A11: R /\ R` = {};
R c= Cl R by PRE_TOPC:18;
then (Cl R)` c= R` by SUBSET_1:12;
then R /\ (Cl R)` = {} by A11,XBOOLE_1:3,26;
hence contradiction by A10;
end;
theorem Th13:
Q is open implies Q /\ Cl K c= Cl(Q /\ K)
proof
assume
A1: Q is open;
let x be object;
assume
A2: x in Q /\ Cl K;
then
A3: x in Cl K by XBOOLE_0:def 4;
reconsider p99= x as Point of TS by A2;
A4: TS is non empty by A2;
A5: x in Q by A2,XBOOLE_0:def 4;
for Q1 being Subset of TS holds Q1 is open implies (p99 in Q1 implies (Q
/\ K) meets Q1)
proof
let Q1 be Subset of TS;
assume
A6: Q1 is open;
assume p99 in Q1;
then p99 in Q1 /\ Q by A5,XBOOLE_0:def 4;
then K meets (Q1 /\ Q) by A1,A3,A4,A6,Th12;
then
A7: K /\ (Q1 /\ Q) <> {};
K /\ (Q1 /\ Q) = (Q /\ K) /\ Q1 by XBOOLE_1:16;
hence thesis by A7;
end;
hence thesis by A4,Th12;
end;
theorem
Q is open implies Cl(Q /\ Cl K) = Cl(Q /\ K)
proof
A1: Cl (Q /\ K) c= Cl(Q /\ Cl K)
proof
let x be object;
assume
A2: x in Cl(Q /\ K);
then reconsider p99= x as Point of TS;
A3: TS is non empty by A2;
for Q1 being Subset of TS holds Q1 is open implies (p99 in Q1 implies
(Q /\ Cl K) meets Q1)
proof
let Q1 be Subset of TS;
assume
A4: Q1 is open;
assume p99 in Q1;
then (Q /\ K) meets Q1 by A2,A3,A4,Th12;
then
A5: (Q /\ K) /\ Q1 <> {};
Q /\ K c= Q /\ Cl K by PRE_TOPC:18,XBOOLE_1:26;
then (Q /\ Cl K) /\ Q1 <> {} by A5,XBOOLE_1:3,26;
hence thesis;
end;
hence thesis by A3,Th12;
end;
assume Q is open;
then Cl(Q /\ Cl K) c= Cl(Cl(Q /\ K)) by Th13,PRE_TOPC:19;
hence thesis by A1;
end;
::
:: INTERIOR OF A SET
::
definition
let GX be TopStruct, R be Subset of GX;
func Int R -> Subset of GX equals
(Cl R`)`;
coherence;
projectivity;
end;
theorem Th15:
Int([#] TS) = [#] TS
proof
Int ([#] TS) = ({} TS)` by PRE_TOPC:22;
hence thesis;
end;
theorem Th16:
Int T c= T
proof
let x be object;
assume
A1: x in Int T;
then reconsider x99= x as Point of GX;
T` c= Cl T` by PRE_TOPC:18;
then not x99 in T` by A1,XBOOLE_0:def 5;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem Th17:
Int K /\ Int L = Int(K /\ L)
proof
Int K /\ Int L = (Cl K` \/ Cl L`)` by XBOOLE_1:53
.= (Cl(K` \/ L`))` by PRE_TOPC:20
.= (Cl (K /\ L)`)` by XBOOLE_1:54;
hence thesis;
end;
registration
let GX;
cluster Int {}GX -> empty;
coherence
proof
{} GX = ([#] GX)` by XBOOLE_1:37
.= (Cl ({}GX)`)` by Th2;
hence thesis;
end;
end;
theorem
Int({} GX) = {} GX;
theorem Th19:
T c= W implies Int T c= Int W
proof
assume T c= W;
then W` c= T` by SUBSET_1:12;
then Cl W` c= Cl T` by PRE_TOPC:19;
hence thesis by SUBSET_1:12;
end;
theorem Th20:
Int T \/ Int W c= Int(T \/ W)
proof
A1: Cl(T` /\ W`) c= Cl T` /\ Cl W` by PRE_TOPC:21;
Int T \/ Int W = ((Cl T`) /\ Cl W`)` by XBOOLE_1:54;
then Int T \/ Int W c= (Cl(T` /\ W`))` by A1,SUBSET_1:12;
hence thesis by XBOOLE_1:53;
end;
theorem
Int(K \ L) c= Int K \ Int L
proof
A1: Int(K \ L) = (Cl (K /\ L`)`)` by SUBSET_1:13
.= (Cl((K`) \/ L``))` by XBOOLE_1:54
.= ((Cl K` \/ Cl L))` by PRE_TOPC:20
.= ((Cl L)`) /\ Int K by XBOOLE_1:53;
L c= Cl L by PRE_TOPC:18;
then
A2: (Cl L)` c= L` by SUBSET_1:12;
Int L c= L by Th16;
then L` c= (Int L)` by SUBSET_1:12;
then ((Cl L)`) c= (Int L)` by A2;
then Int(K \ L) c= Int K /\ (Int L)` by A1,XBOOLE_1:26;
hence thesis by SUBSET_1:13;
end;
registration
let T be TopSpace, K be Subset of T;
cluster Int K -> open;
coherence;
end;
registration
let T be TopSpace;
cluster empty -> open for Subset of T;
coherence
proof
let S be Subset of T;
Int {}T = {}T;
hence thesis;
end;
cluster [#]T -> open;
coherence
proof
Int [#]T = [#]T by Th15;
hence thesis;
end;
end;
registration
let T be TopSpace;
cluster open closed for Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster non empty open closed for Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
theorem Th22:
x in Int K iff ex Q st Q is open & Q c= K & x in Q
proof
thus x in Int K implies ex Q st Q is open & Q c= K & x in Q by Th16;
given Q such that
A1: Q is open and
A2: Q c= K and
A3: x in Q;
K` c= Q` by A2,SUBSET_1:12;
then Cl K` c= Cl Q` by PRE_TOPC:19;
then Cl K` c= Q` by A1,PRE_TOPC:22;
then Q`` c= (Cl K`)` by SUBSET_1:12;
hence thesis by A3;
end;
theorem Th23:
(R is open implies Int R = R) & (Int P = P implies P is open)
proof
hereby
assume R is open;
then R` is closed by Th4;
then Cl R` = R` by PRE_TOPC:22;
hence Int R = R;
end;
thus thesis;
end;
theorem
S is open & S c= T implies S c= Int T
proof
assume that
A1: S is open and
A2: S c= T;
Int S = S by A1,Th23;
hence thesis by A2,Th19;
end;
theorem
P is open iff for x holds x in P iff ex Q st Q is open & Q c= P & x in Q
proof
thus P is open implies for x holds x in P iff ex Q st Q is open & Q c= P & x
in Q;
assume
A1: for x holds x in P iff ex Q st Q is open & Q c= P & x in Q;
now
let x be object;
x in P iff ex Q st Q is open & Q c= P & x in Q by A1;
hence x in P iff x in Int P by Th22;
end;
hence thesis by TARSKI:2;
end;
theorem Th26:
Cl Int T = Cl Int Cl Int T
proof
Int Int T c= Int Cl Int T by Th19,PRE_TOPC:18;
then
A1: Cl Int T c= Cl Int Cl Int T by PRE_TOPC:19;
Cl Int Cl Int T c= Cl Cl Int T by Th16,PRE_TOPC:19;
hence thesis by A1;
end;
theorem
R is open implies Cl Int Cl R = Cl R
proof
assume
A1: R is open;
then Cl Int Cl R = Cl Int Cl Int R by Th23
.= Cl Int R by Th26
.= Cl R by A1,Th23;
hence thesis;
end;
::
:: FRONTIER OF A SET
::
definition
let GX be TopStruct, R be Subset of GX;
func Fr R -> Subset of GX equals
Cl R /\ Cl R`;
coherence;
end;
registration
let T be TopSpace, A be Subset of T;
cluster Fr A -> closed;
coherence;
end;
theorem Th28:
for GX being non empty TopSpace, R being Subset of GX, p being
Point of GX holds p in Fr R iff for S being Subset of GX st S is open & p in S
holds R meets S & R` meets S
proof
let GX be non empty TopSpace, R be Subset of GX, p be Point of GX;
hereby
assume
A1: p in Fr R;
then
A2: p in Cl R` by XBOOLE_0:def 4;
let S be Subset of GX;
assume that
A3: S is open and
A4: p in S;
p in Cl R by A1,XBOOLE_0:def 4;
hence R meets S & R` meets S by A3,A4,A2,Th12;
end;
assume
A5: for S being Subset of GX st S is open & p in S holds R meets S & R`
meets S;
then for S being Subset of GX st S is open & p in S holds R` meets S;
then
A6: p in Cl R` by Th12;
for S being Subset of GX st S is open & p in S holds R meets S by A5;
then p in Cl R by Th12;
hence thesis by A6,XBOOLE_0:def 4;
end;
theorem
Fr T = Fr T`;
theorem
Fr T = Cl(T`) /\ T \/ (Cl T \ T)
proof
for x being object holds x in Fr T iff x in ((Cl(T`) /\ T) \/ (Cl T\T))
proof
let x be object;
A1: T` c= Cl(T`) by PRE_TOPC:18;
thus x in Fr T implies x in ((Cl(T`) /\ T) \/ (Cl T \ T))
proof
assume
A2: x in Fr T;
then reconsider x99= x as Point of GX;
x99 in Cl T & x99 in Cl(T`) & x99 in T or x99 in Cl T & x99 in Cl(T`
) & x99 in T` by A2,SUBSET_1:29,XBOOLE_0:def 4;
then x99 in Cl(T`) /\ T or not x99 in T & x99 in Cl T by XBOOLE_0:def 4;
then x99 in (Cl(T`) /\ T) or x99 in (Cl T \ T) by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
A3: T c= Cl T by PRE_TOPC:18;
thus x in ((Cl(T`) /\ T) \/ (Cl T \ T)) implies x in Fr T
proof
assume
A4: x in (Cl(T`) /\ T) \/ (Cl T \ T);
then reconsider x99= x as Point of GX;
x99 in (Cl(T`) /\ T) or x99 in (Cl T \ T) by A4,XBOOLE_0:def 3;
then x99 in Cl(T`) & x99 in T or x99 in Cl T & not x99 in T by
XBOOLE_0:def 4,def 5;
then x99 in Cl(T`) & x99 in T or x99 in Cl T & x99 in T` by SUBSET_1:29;
hence thesis by A3,A1,XBOOLE_0:def 4;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th31:
Cl T = T \/ Fr T
proof
A1: (T \/ Cl T) /\ (T \/ Cl(T`)) = Cl T /\ (T \/ Cl(T`)) by PRE_TOPC:18
,XBOOLE_1:12;
T \/ (Cl T \ T) c= T \/ (Cl T /\ Cl(T`))
proof
let x be object;
assume
A2: x in T \/ (Cl T \ T);
then reconsider x99=x as Point of GX;
x99 in T or x99 in Cl T \ T by A2,XBOOLE_0:def 3;
then
A3: x99 in T or x99 in Cl T & x99 in T` by XBOOLE_0:def 5;
T` c= Cl(T`) by PRE_TOPC:18;
then x99 in T or x99 in (Cl T /\ Cl (T`)) by A3,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then
A4: Cl T c= T \/ Fr T by PRE_TOPC:18,XBOOLE_1:45;
T \/ Fr T = (T \/ Cl T) /\ (T \/ Cl (T`)) by XBOOLE_1:24;
then T \/ Fr T c= Cl T by A1,XBOOLE_1:17;
hence thesis by A4;
end;
theorem Th32:
Fr(K /\ L) c= Fr K \/ Fr L
proof
Cl(K /\ L) c= Cl K by PRE_TOPC:19,XBOOLE_1:17;
then
A1: Cl(K /\ L) /\ Cl(K`) c= Cl K /\ Cl(K`) by XBOOLE_1:26;
Cl(K /\ L) c= Cl L by PRE_TOPC:19,XBOOLE_1:17;
then
A2: Cl(K /\ L) /\ Cl(L`) c= Cl L /\ Cl(L`) by XBOOLE_1:26;
Fr(K /\ L) = Cl(K /\ L) /\ Cl((K`) \/ L`) by XBOOLE_1:54
.= Cl(K /\ L) /\ (Cl(K`) \/ Cl L`) by PRE_TOPC:20
.=(Cl(K /\ L) /\ Cl(K`)) \/ (Cl(K /\ L) /\ Cl(L`)) by XBOOLE_1:23;
hence thesis by A1,A2,XBOOLE_1:13;
end;
theorem Th33:
Fr(K \/ L) c= Fr K \/ Fr L
proof
Cl((K`) /\ L`) c= Cl K` by PRE_TOPC:19,XBOOLE_1:17;
then
A1: Cl((K`) /\ L`) /\ Cl K c= Cl(K`) /\ Cl K by XBOOLE_1:26;
Cl((K`) /\ L`) c= Cl L` by PRE_TOPC:19,XBOOLE_1:17;
then
A2: Cl((K`) /\ L`) /\ Cl L c= Cl(L`) /\ Cl L by XBOOLE_1:26;
Fr(K \/ L) = (Cl K \/ Cl L) /\ Cl((K \/ L)`) by PRE_TOPC:20
.= Cl((K`) /\ L`) /\ (Cl K \/ Cl L) by XBOOLE_1:53
.= (Cl((K`) /\ L`) /\ Cl K) \/ (Cl((K`) /\ L`) /\ Cl L) by XBOOLE_1:23;
hence thesis by A1,A2,XBOOLE_1:13;
end;
theorem Th34:
Fr Fr T c= Fr T
proof
let x be object;
assume x in Fr(Fr T);
then
A1: x in Cl(Cl T /\ Cl(T`)) by XBOOLE_0:def 4;
Cl(Cl T /\ Cl(T`)) c= Cl(Cl T) /\ Cl(Cl(T`)) by PRE_TOPC:21;
hence thesis by A1;
end;
theorem
R is closed implies Fr R c= R
proof
assume
A1: R is closed;
let x be object;
Cl R = R by A1,PRE_TOPC:22;
hence thesis by XBOOLE_0:def 4;
end;
Lm1: Fr K c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L)
proof
let x be object;
A1: (L`) /\ (K`) = (K \/ L)` by XBOOLE_1:53;
assume
A2: x in Fr K;
then reconsider x99= x as Point of TS;
A3: TS is non empty by A2;
assume
A4: not x in (Fr(K \/ L) \/ Fr(K /\ L)) \/ (Fr K /\ Fr L);
then
A5: not x99 in (Fr(K \/ L) \/ Fr(K /\ L)) by XBOOLE_0:def 3;
then not x99 in Fr(K \/ L) by XBOOLE_0:def 3;
then consider Q1 being Subset of TS such that
A6: Q1 is open and
A7: x99 in Q1 and
A8: (K \/ L) misses Q1 or ((K \/ L)`) misses Q1 by A3,Th28;
(K \/ L) /\ Q1 = {} or ((K \/ L)`) /\ Q1 = {} by A8;
then
A9: (K /\ Q1) \/ (Q1 /\ L)={} or (L`) /\ ((K`) /\ Q1)={} by A1,XBOOLE_1:16,23;
not x99 in (Fr K /\ Fr L) by A4,XBOOLE_0:def 3;
then not x99 in Fr L by A2,XBOOLE_0:def 4;
then consider Q3 being Subset of TS such that
A10: Q3 is open and
A11: x99 in Q3 and
A12: L misses Q3 or (L`) misses Q3 by A3,Th28;
K meets Q1 by A2,A3,A6,A7,Th28;
then
A13: K /\ Q1 <> {};
A14: now
assume L /\ Q3 = {};
then Q3 misses L``;
then
A15: Q3 c= L` by SUBSET_1:24;
((K`) /\ Q1) /\ ((L`) /\ Q3) = {} /\ Q3 by A9,A13,XBOOLE_1:16;
then ((K`) /\ Q1) /\ Q3 = {} by A15,XBOOLE_1:28;
hence (K`) /\ (Q1 /\ Q3) = {} by XBOOLE_1:16;
end;
A16: (L`) \/ (K`) = (K /\ L)` by XBOOLE_1:54;
not x99 in Fr(K /\ L) by A5,XBOOLE_0:def 3;
then consider Q2 being Subset of TS such that
A17: Q2 is open and
A18: x99 in Q2 and
A19: (K /\ L) misses Q2 or ((K /\ L)`) misses Q2 by A3,Th28;
(K /\ L) /\ Q2 = {} or ((K /\ L)`) /\ Q2 = {} by A19;
then
A20: (K /\ Q2) /\ L={} or ((K`) /\ Q2) \/ (Q2 /\ (L`))={} by A16,XBOOLE_1:16,23
;
x99 in Q1 /\ Q3 by A7,A11,XBOOLE_0:def 4;
then (K`) meets (Q1 /\ Q3) by A2,A3,A6,A10,Th28;
then
A21: Q3 c= L by A12,A14,SUBSET_1:24;
(K`) meets Q2 by A2,A3,A17,A18,Th28;
then (K`) /\ Q2 <> {};
then (K /\ (Q2 /\ L)) /\ Q3 = {} /\ Q3 by A20,XBOOLE_1:16;
then K /\ ((Q2 /\ L) /\ Q3) = {} by XBOOLE_1:16;
then K /\ (Q2 /\ (L /\ Q3)) = {} by XBOOLE_1:16;
then K /\ (Q2 /\ Q3) = {} by A21,XBOOLE_1:28;
then
A22: K misses (Q2 /\ Q3);
x99 in Q2 /\ Q3 by A18,A11,XBOOLE_0:def 4;
hence contradiction by A2,A3,A17,A10,A22,Th28;
end;
theorem
Fr K \/ Fr L = Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L)
proof
A1: Fr L c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) by Lm1;
A2: Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) c= Fr K \/ Fr L
proof
let x be object;
A3: now
assume x in (Fr K /\ Fr L);
then x in Fr K by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
A4: now
assume
A5: x in Fr(K \/ L);
Fr(K \/ L) c= (Fr K \/ Fr L) by Th33;
hence thesis by A5;
end;
A6: now
assume
A7: x in Fr(K /\ L);
Fr(K /\ L) c= (Fr K \/ Fr L) by Th32;
hence thesis by A7;
end;
assume x in (Fr(K \/ L) \/ Fr(K /\ L)) \/ (Fr K /\ Fr L);
then x in (Fr(K \/ L) \/ Fr(K /\ L)) or x in (Fr K /\ Fr L) by
XBOOLE_0:def 3;
hence thesis by A4,A6,A3,XBOOLE_0:def 3;
end;
Fr K c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) by Lm1;
then Fr K \/ Fr L c= Fr(K \/ L) \/ Fr(K /\ L) \/ (Fr K /\ Fr L) by A1,
XBOOLE_1:8;
hence thesis by A2;
end;
theorem
Fr Int T c= Fr T
proof
let x be object;
assume
A1: x in Fr(Int T);
then
A2: x in Cl(T`) by XBOOLE_0:def 4;
Int T = (Cl T`)`;
then
A3: Cl((Cl T`)`) c= Cl T by Th16,PRE_TOPC:19;
x in Cl((Cl T`)`) by A1,XBOOLE_0:def 4;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
theorem
Fr Cl T c= Fr T
proof
T c= Cl T by PRE_TOPC:18;
then (Cl T)` c= T` by SUBSET_1:12;
then Cl((Cl T)`) c= Cl(T`) by PRE_TOPC:19;
hence thesis by XBOOLE_1:26;
end;
theorem Th39:
Int T misses Fr T
proof
Fr T = Cl T /\ (((Cl T`)`)`) .= Cl T \ ((Cl T`)`) by SUBSET_1:13;
hence thesis by XBOOLE_1:79;
end;
theorem Th40:
Int T = T \ Fr T
proof
(Cl T`)` \/ (Cl T)` = (Cl T /\ Cl T`)` by XBOOLE_1:54;
then
A1: T \ Fr T = T /\ ((Cl T`)` \/ (Cl T)`) by SUBSET_1:13
.= (T /\ (Cl T)`) \/ (T /\ Int T) by XBOOLE_1:23;
T c= Cl T by PRE_TOPC:18;
then
A2: T misses (Cl T)` by SUBSET_1:24;
Int T = T /\ Int T by Th16,XBOOLE_1:28;
then T \ Fr T = {} \/ Int T by A1,A2;
hence thesis;
end;
Lm2: Fr T = Cl T \ Int T
proof
Fr T = Cl T /\ (Int T)` .= Cl T \ Int T by SUBSET_1:13;
hence thesis;
end;
Lm3: Cl Fr K = Fr K
proof
A1: Cl Cl K` = Cl K`;
Cl Cl K = Cl K;
hence thesis by A1,Th7;
end;
Lm4: Int Fr Fr K = {}
proof
set x9 = the Element of Int(Fr(Fr K));
assume
A1: Int Fr Fr K <> {};
then reconsider x = x9 as Point of TS by TARSKI:def 3;
A2: TS is non empty by A1;
A3: Int(Fr(Fr K)) c= Fr(Fr K) by Th16;
then x in Fr(Fr K) by A1;
then (Fr K)` meets Int(Fr(Fr K)) by A1,A2,Th28;
then
A4: (Fr K)` /\ Int(Fr(Fr K)) <> {};
Fr(Fr K) c= Fr K by Th34;
then Int(Fr(Fr K)) c= Fr K by A3;
then
A5: (Fr K)` /\ Fr K <> {} by A4,XBOOLE_1:3,26;
Fr K misses (Fr K)` by XBOOLE_1:79;
hence contradiction by A5;
end;
theorem
Fr Fr Fr K = Fr Fr K
proof
A1: Int Fr Fr K = {} by Lm4;
Fr Fr Fr K = Cl(Fr(Fr K)) \ Int(Fr(Fr K)) by Lm2
.= Fr Fr K by A1,Lm3;
hence thesis;
end;
Lm5: for X, Y, Z being set holds X c= Z & Y = Z \ X implies X c= Z \ Y
proof
let X, Y, Z be set;
assume that
A1: X c= Z and
A2: Y = Z \ X;
let x be object;
assume
A3: x in X;
then not x in Y by A2,XBOOLE_0:def 5;
hence thesis by A1,A3,XBOOLE_0:def 5;
end;
theorem Th42:
P is open iff Fr P = Cl P \ P
proof
A1: Fr P misses (Fr P)` by XBOOLE_1:79;
A2: Int P c= P by Th16;
hereby
assume P is open;
then P = Int P by Th23;
hence Fr P = Cl P \ P by Lm2;
end;
assume
A3: Fr P = Cl P \ P;
Cl P \ Fr P = (P \/ Fr P) \ Fr P by Th31
.= (Fr P)` /\ (P \/ Fr P) by SUBSET_1:13
.= (P /\ (Fr P)`) \/ ((Fr P)` /\ (Fr P)) by XBOOLE_1:23
.= (P \ Fr P) \/ (Fr P /\ (Fr P)`) by SUBSET_1:13
.= Int P \/ (Fr P /\ (Fr P)`) by Th40
.= Int P \/ {} TS by A1
.= Int P;
then P c= Int P by A3,Lm5,PRE_TOPC:18;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th43:
P is closed iff Fr P = P \ Int P
proof
A1: (P`) misses P by XBOOLE_1:79;
(P`) /\ Int P c= (P`) /\ P by Th16,XBOOLE_1:26;
then
A2: (P`) /\ Int P c= {} TS by A1;
thus P is closed implies Fr P = P \ Int P
proof
assume P is closed;
then P = Cl P by PRE_TOPC:22;
hence thesis by Lm2;
end;
A3: (P``) \/ (Int P)` = ((P`) /\ Int P)` by XBOOLE_1:54;
assume Fr P = P \ Int P;
then Cl P = P \/ (P \ Int P) by Th31
.= P \/ ((Int P)` /\ P) by SUBSET_1:13
.= (P \/ (Int P)`) /\ (P \/ P) by XBOOLE_1:24
.= ({} TS)` /\ P by A2,A3
.= P by XBOOLE_1:28;
hence thesis;
end;
::
:: DENSE, BOUNDARY AND NOWHEREDENSE SETS
::
definition
let GX be TopStruct, R be Subset of GX;
attr R is dense means
Cl R = [#] GX;
end;
registration
let GX;
cluster [#]GX -> dense;
coherence
by Th2;
cluster dense for Subset of GX;
existence
proof
take [#]GX;
thus thesis;
end;
end;
theorem
R is dense & R c= S implies S is dense
proof
assume that
A1: R is dense and
A2: R c= S;
Cl R = [#] GX by A1;
then [#] GX c= Cl S by A2,PRE_TOPC:19;
then [#] GX = Cl S;
hence thesis;
end;
theorem Th45:
P is dense iff for Q st Q <> {} & Q is open holds P meets Q
proof
hereby
assume P is dense;
then
A1: Cl P = [#] TS;
let Q;
assume that
A2: Q<>{} and
A3: Q is open;
set x = the Element of Q;
x in Q by A2;
then
A4: TS is non empty;
x in Cl P by A2,A1,TARSKI:def 3;
hence P meets Q by A2,A3,A4,Th12;
end;
assume
A5: for Q st Q <> {} & Q is open holds P meets Q;
[#] TS c= Cl P
proof
let x be object;
A6: for C be Subset of TS st C is open & x in C holds P meets C by A5;
assume
A7: x in [#] TS;
then TS is non empty;
hence thesis by A7,A6,Th12;
end;
then Cl P = [#] TS;
hence thesis;
end;
theorem Th46:
P is dense implies for Q holds Q is open implies Cl Q = Cl(Q /\ P)
proof
assume
A1: P is dense;
let Q;
assume
A2: Q is open;
thus Cl Q c= Cl(Q /\ P)
proof
let x be object;
assume
A3: x in Cl Q;
then
A4: TS is non empty;
now
let Q1 be Subset of TS;
assume
A5: Q1 is open;
assume x in Q1;
then Q meets Q1 by A3,A4,A5,Th12;
then Q /\ Q1 <> {};
then P meets (Q /\ Q1) by A1,A2,A5,Th45;
then
A6: P /\ (Q /\ Q1) <> {};
P /\ (Q /\ Q1) = (Q /\ P) /\ Q1 by XBOOLE_1:16;
hence (Q /\ P) meets Q1 by A6;
end;
hence thesis by A3,A4,Th12;
end;
thus thesis by PRE_TOPC:19,XBOOLE_1:17;
end;
theorem
P is dense & Q is dense & Q is open implies P /\ Q is dense
by Th46;
definition
let GX be TopStruct, R be Subset of GX;
attr R is boundary means
R` is dense;
end;
registration
let GX;
cluster empty -> boundary for Subset of GX;
coherence
proof
let A be Subset of GX;
assume A is empty;
hence Cl A` = [#]GX by Th2;
end;
end;
theorem Th48:
R is boundary iff Int R = {}
proof
R is boundary iff R` is dense;
then R is boundary iff Cl(R`) = [#] GX;
then R is boundary iff (Cl R`)` = ([#] GX)` by SUBSET_1:42;
hence thesis by XBOOLE_1:37;
end;
registration
let GX;
cluster boundary for Subset of GX;
existence
proof
take {}GX;
thus thesis;
end;
end;
registration
let GX;
let R be boundary Subset of GX;
cluster Int R -> empty;
coherence by Th48;
end;
theorem Th49:
P is boundary & Q is boundary & Q is closed implies P \/ Q is boundary
proof
assume that
A1: P is boundary and
A2: Q is boundary and
A3: Q is closed;
A4: Cl((P`) \ Q) = Cl(((P`) /\ Q`)) by SUBSET_1:13;
P` is dense by A1;
then
A5: [#] TS \ Q = Cl(P`) \ Q;
A6: Cl(P`) \ Cl Q c= Cl((P`) \ Q) by Th6;
Q` is dense by A2;
then
A7: Cl(Q`) = [#] TS;
Cl(P`) \ Q = Cl(P`) \ Cl Q by A3,PRE_TOPC:22;
then [#] TS \ Q c= Cl((P \/ Q)`) by A5,A6,A4,XBOOLE_1:53;
then Cl(Q`) c= Cl(Cl((P \/ Q)`)) by PRE_TOPC:19;
then [#] TS = Cl((P \/ Q)`) by A7;
then (P \/ Q)` is dense;
hence thesis;
end;
theorem
P is boundary iff for Q st Q c= P & Q is open holds Q = {}
proof
hereby
assume P is boundary;
then
A1: P` is dense;
let Q;
assume that
A2: Q c= P and
A3: Q is open and
A4: Q <> {};
Q meets P` by A1,A3,A4,Th45;
hence contradiction by A2,SUBSET_1:24;
end;
assume
A5: for Q st Q c= P & Q is open holds Q={};
assume not P is boundary;
then not P` is dense;
then consider C being Subset of TS such that
A6: C <> {} and
A7: C is open and
A8: (P`) misses C by Th45;
C c= P by A8,SUBSET_1:24;
hence contradiction by A5,A6,A7;
end;
theorem
P is closed implies (P is boundary iff for Q st Q <> {} & Q is open ex
G being Subset of TS st G c= Q & G <> {} & G is open & P misses G)
proof
assume
A1: P is closed;
hereby
assume P is boundary;
then
A2: P` is dense;
A3: P misses (P`) by XBOOLE_1:79;
let Q such that
A4: Q <> {} and
A5: Q is open;
P /\ ((P`) /\ Q) = (P /\ (P`)) /\ Q by XBOOLE_1:16
.= {} TS /\ Q by A3
.= {};
then
A6: P misses ((P`) /\ Q);
(P`) meets Q by A2,A4,A5,Th45;
then (P`) /\ Q <> {};
hence ex G being Subset of TS st G c= Q & G <> {} & G is open & P misses G
by A1,A5,A6,XBOOLE_1:17;
end;
assume
A7: for Q st Q <> {} & Q is open ex G being Subset of TS st G c= Q & G
<> {} & G is open & P misses G;
now
let Q such that
A8: Q <> {} and
A9: Q is open;
consider G being Subset of TS such that
A10: G c= Q and
A11: G <> {} and
G is open and
A12: P misses G by A7,A8,A9;
G misses (P``) by A12;
then G c= P` by SUBSET_1:24;
hence (P`) meets Q by A10,A11,XBOOLE_1:67;
end;
then P` is dense by Th45;
hence thesis;
end;
theorem
R is boundary iff R c= Fr R
proof
A1: Cl R /\ Cl(R`) c= Cl(R`) by XBOOLE_1:17;
hereby
assume R is boundary;
then R` is dense;
then Cl R /\ Cl R` = Cl R /\ ([#] GX);
then Cl R = Cl R /\ Cl R` by XBOOLE_1:28;
hence R c= Fr R by PRE_TOPC:18;
end;
A2: R` c= Cl(R`) by PRE_TOPC:18;
assume R c= Fr R;
then R c= Cl(R`) by A1;
then R \/ (R`) c= Cl(R`) by A2,XBOOLE_1:8;
then [#] GX c= Cl(R`) by PRE_TOPC:2;
then [#] GX = Cl(R`);
then R` is dense;
hence thesis;
end;
registration
let GX be non empty TopSpace;
cluster [#]GX -> non boundary;
coherence
proof
Int [#]GX <> {} by Th15;
hence thesis;
end;
cluster non boundary non empty for Subset of GX;
existence
proof
take [#]GX;
thus thesis;
end;
end;
definition
let GX be TopStruct, R be Subset of GX;
attr R is nowhere_dense means
Cl R is boundary;
end;
registration
let TS;
cluster empty -> nowhere_dense for Subset of TS;
coherence
by PRE_TOPC:22;
end;
registration
let TS;
cluster nowhere_dense for Subset of TS;
existence
proof
take {}TS;
thus thesis;
end;
end;
theorem
P is nowhere_dense & Q is nowhere_dense implies P \/ Q is nowhere_dense
proof
assume that
A1: P is nowhere_dense and
A2: Q is nowhere_dense;
A3: Cl Q is boundary by A2;
Cl P is boundary by A1;
then Cl P \/ Cl Q is boundary by A3,Th49;
then Cl(P \/ Q) is boundary by PRE_TOPC:20;
hence thesis;
end;
theorem Th54:
R is nowhere_dense implies R` is dense
proof
assume R is nowhere_dense;
then Cl R is boundary;
then (Cl R)` is dense;
then
A1: Cl((Cl R)`) = [#] GX;
R c= Cl R by PRE_TOPC:18;
then (Cl R)` c= R` by SUBSET_1:12;
then [#] GX c= Cl(R`) by A1,PRE_TOPC:19;
then [#] GX= Cl(R`);
hence thesis;
end;
registration
let TS;
let R be nowhere_dense Subset of TS;
cluster R` -> dense;
coherence by Th54;
end;
theorem
R is nowhere_dense implies R is boundary
by Th54;
registration
let TS;
cluster nowhere_dense -> boundary for Subset of TS;
coherence;
end;
theorem Th56:
S is boundary & S is closed implies S is nowhere_dense
by PRE_TOPC:22;
registration
let TS;
cluster boundary closed -> nowhere_dense for Subset of TS;
coherence by Th56;
end;
theorem
R is closed implies (R is nowhere_dense iff R = Fr R)
proof
assume R is closed;
then
A1: R = Cl R by PRE_TOPC:22;
hereby
assume R is nowhere_dense;
then Cl R is boundary;
then (Cl R)` is dense;
then Fr R = R /\ [#] GX by A1;
hence R = Fr R by XBOOLE_1:28;
end;
assume R = Fr R;
then R = R \ Int R by A1,Lm2;
then Int(Cl R) = {} by A1,Th16,XBOOLE_1:38;
then Cl R is boundary by Th48;
hence thesis;
end;
theorem Th58:
P is open implies Fr P is nowhere_dense
proof
A1: Int(Cl P) c= Cl P by Th16;
assume P is open;
then
A2: Int P = P by Th23;
then P misses Fr P by Th39;
then
A3: P /\ Fr P = {} TS;
Int (P /\ Fr P) = P /\ Int(Fr P) by A2,Th17;
then P /\ Int(Fr P) = {} by A3;
then
A4: P misses Int(Fr P);
Int(Fr P) c= Int(Cl P) by Th19,XBOOLE_1:17;
then
A5: Int(Fr P) c= Cl P by A1;
Fr P is boundary
proof
set x = the Element of Int(Fr P);
assume
A6: not Fr P is boundary;
then
A7: TS is non empty;
A8: Int (Fr P) <> {} by A6,Th48;
then x in Cl P by A5;
hence contradiction by A4,A8,A7,Th12;
end;
hence thesis;
end;
registration
let TS;
let P be open Subset of TS;
cluster Fr P -> nowhere_dense;
coherence by Th58;
end;
theorem Th59:
P is closed implies Fr P is nowhere_dense
proof
assume P is closed;
then Fr P` is nowhere_dense;
hence thesis;
end;
registration
let TS;
let P be closed Subset of TS;
cluster Fr P -> nowhere_dense;
coherence by Th59;
end;
theorem Th60:
P is open & P is nowhere_dense implies P = {}
proof
assume that
A1: P is open and
A2: P is nowhere_dense and
A3: P <> {};
P meets P` by A1,A2,A3,Th45;
hence contradiction by XBOOLE_1:79;
end;
registration
let TS;
cluster open nowhere_dense -> empty for Subset of TS;
coherence by Th60;
end;
::
:: CLOSED AND OPEN DOMAIN, DOMAIN
::
definition
let GX be TopStruct, R be Subset of GX;
attr R is condensed means
Int Cl R c= R & R c= Cl Int R;
attr R is closed_condensed means
R = Cl Int R;
attr R is open_condensed means
R = Int Cl R;
end;
theorem
R is open_condensed iff R` is closed_condensed;
theorem
R is closed_condensed implies Fr Int R = Fr R;
theorem
R is closed_condensed implies Fr R c= Cl Int R
by XBOOLE_1:17;
theorem Th64:
R is open_condensed implies Fr R = Fr Cl R & Fr Cl R = Cl R \ R
by Lm2;
theorem
R is open & R is closed implies (R is closed_condensed iff R is
open_condensed)
by PRE_TOPC:22,Th23;
theorem
(R is closed & R is condensed implies R is closed_condensed) &
(P is closed_condensed implies P is closed & P is condensed)
proof
hereby
assume that
A1: R is closed and
A2: R is condensed;
A3: R = Cl R by A1,PRE_TOPC:22;
then Int R c= R by A2;
then
A4: Cl(Int R) c= R by A3,PRE_TOPC:19;
R c= Cl(Int R) by A2;
then Cl(Int R) = R by A4;
hence R is closed_condensed;
end;
assume
A5: P is closed_condensed;
Fr(Int P) = Cl(Int P) \ Int(Int P) by Lm2;
then Fr P = Cl(Int P) \ Int(Int P) by A5
.= P \ Int P by A5;
then P is closed by Th43;
then Cl P = P by PRE_TOPC:22;
then
A6: Int Cl P c= P by Th16;
Cl Int P = P by A5;
hence thesis by A6;
end;
theorem
(R is open & R is condensed implies R is open_condensed) & (P is
open_condensed implies P is open & P is condensed)
proof
hereby
assume that
A1: R is open and
A2: R is condensed;
R = Int R by A1,Th23;
then
A3: R c= Int(Cl R) by Th19,PRE_TOPC:18;
Int Cl R c= R by A2;
then Int Cl R = R by A3;
hence R is open_condensed;
end;
assume
A4: P is open_condensed;
then
A5: Fr Cl P = Cl P \ P by Th64;
Fr P = Fr Cl P by A4;
then P is open by A5,Th42;
then Int P = P by Th23;
then
A6: P c= Cl Int P by PRE_TOPC:18;
P = Int(Cl P) by A4;
hence thesis by A6;
end;
theorem Th68:
P is closed_condensed & Q is closed_condensed implies P \/ Q is
closed_condensed
proof
assume that
A1: P is closed_condensed and
A2: Q is closed_condensed;
A3: Q = Cl(Int Q) by A2;
P = Cl(Int P) by A1;
then P \/ Q = Cl(Int P \/ Int Q) by A3,PRE_TOPC:20;
then
A4: P \/ Q c= Cl(Int(P \/ Q)) by Th20,PRE_TOPC:19;
A5: Cl(Int(P \/ Q)) c= Cl(P \/ Q) by Th16,PRE_TOPC:19;
A6: Q is closed by A2;
P is closed by A1;
then Cl(Int(P \/ Q)) c= P \/ Q by A5,A6,PRE_TOPC:22;
then P \/ Q = Cl(Int(P \/ Q)) by A4;
hence thesis;
end;
theorem
P is open_condensed & Q is open_condensed implies P /\ Q is open_condensed
proof
A1: P` \/ Q` = (P /\ Q)` by XBOOLE_1:54;
assume that
A2: P is open_condensed and
A3: Q is open_condensed;
A4: Q` is closed_condensed by A3;
P` is closed_condensed by A2;
then P` \/ Q` is closed_condensed by A4,Th68;
hence thesis by A1;
end;
theorem
P is condensed implies Int Fr P = {}
proof
set x = the Element of Int(Fr P);
assume
A1: P is condensed;
then P c= Cl(Int P);
then
A2: (Cl(Int P))` c= P` by SUBSET_1:12;
assume
A3: Int(Fr P) <> {};
then reconsider x99= x as Point of TS by TARSKI:def 3;
A4: Int(Fr P) = (Cl(((Cl P)`) \/ (Cl P`)`))` by XBOOLE_1:54
.= (Cl(((Cl P)`)) \/ Cl((Cl P`))`)` by PRE_TOPC:20
.= Int(Cl P) /\ (Cl(Int P))` by XBOOLE_1:53;
then
A5: x99 in Int(Cl P) by A3,XBOOLE_0:def 4;
A6: x99 in (Cl(Int P))` by A4,A3,XBOOLE_0:def 4;
Int(Cl P) c= P by A1;
hence contradiction by A2,A5,A6,XBOOLE_0:def 5;
end;
theorem
R is condensed implies Int R is condensed & Cl R is condensed
proof
Cl(Int R) c= Cl R by Th16,PRE_TOPC:19;
then
A1: Int(Cl(Int R)) c= Int(Cl R) by Th19;
A2: R c= Cl R by PRE_TOPC:18;
then (Cl R)` c= R` by SUBSET_1:12;
then Cl((Cl R)`) c= Cl(R`) by PRE_TOPC:19;
then (Cl R`)` c= (Cl(((Cl R)`)))` by SUBSET_1:12;
then
A3: Cl(Int R) c= Cl((Cl((Cl R)`))`) by PRE_TOPC:19;
assume
A4: R is condensed;
then
A5: R c= Cl(Int R);
then Cl R c= Cl(Cl(Int R)) by PRE_TOPC:19;
then
A6: Cl R c= Cl(Int(Cl R)) by A3;
A7: Int(Cl R) c= R by A4;
then Int(Int(Cl R)) c= Int R by Th19;
then
A8: Int(Cl(Int R)) c= Int R by A1;
Int R c= R by Th16;
then
A9: Int R c= Cl(Int(Int R)) by A5;
(Int(Cl(Cl R))) c= Cl R by A7,A2;
hence thesis by A9,A6,A8;
end;