:: Components and Basis of Topological Spaces
:: by Robert Milewski
::
:: Received June 22, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1, TARSKI,
SUBSET_1, MARGREL1, FINSET_1, FINSEQ_2, CARD_1, SETFAM_1, STRUCT_0,
ZFMISC_1, FUNCOP_1, XBOOLEAN, EQREL_1, ORDERS_2, WAYBEL23, YELLOW_0,
LATTICES, ORDINAL2, WAYBEL_0, WAYBEL_3, WAYBEL_8, RCOMP_1, PRE_TOPC,
RLVECT_3, CANTOR_1, YELLOW15;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, SETFAM_1, DOMAIN_1,
CARD_1, NUMBERS, FINSET_1, STRUCT_0, MARGREL1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, EQREL_1, FUNCOP_1,
CARD_3, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2, YELLOW_0, WAYBEL_0,
WAYBEL_3, WAYBEL_8, WAYBEL23;
constructors XXREAL_0, FINSEQ_4, REALSET1, VALUAT_1, TOPS_2, CANTOR_1,
WAYBEL_8, WAYBEL23, RELSET_1, NUMBERS;
registrations SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, FINSEQ_1, MARGREL1,
FINSEQ_2, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, WAYBEL_3, WAYBEL23,
ORDINAL1, PRE_TOPC, ZFMISC_1, CARD_1, RELAT_1, FINSEQ_3;
requirements NUMERALS, REAL, SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, XBOOLE_0, MARGREL1;
equalities XBOOLE_0, MARGREL1, XBOOLEAN, STRUCT_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, SETFAM_1, ZFMISC_1, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2,
MSSUBFAM, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, EQREL_1, FUNCOP_1,
CARD_1, CARD_4, T_0TOPSP, PRE_TOPC, TOPS_2, CANTOR_1, YELLOW_0, YELLOW_8,
YELLOW_9, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL23, XBOOLE_0, XBOOLE_1,
SUBSET_1, ORDINAL1, XBOOLEAN;
schemes FUNCT_2, PRE_CIRC, FINSEQ_1, FRAENKEL;
begin :: Preliminaries
scheme
SeqLambda1C{ i() -> Nat, D() -> non empty set, C[object],
F, G(object)->set } :
ex p be FinSequence of D() st len p = i() & for i be Nat st i in Seg i(
) holds (C[i] implies p.i = F(i)) & (not C[i] implies p.i = G(i))
provided
A1: for i be Nat st i in Seg i() holds (C[i] implies F(i) in D()) & (not
C[i] implies G(i) in D())
proof
A2: for x be object st x in Seg i()
holds (C[x] implies F(x) in D()) & (not C[x
] implies G(x) in D()) by A1;
consider p be Function of Seg i(),D() such that
A3: for x be object st x in Seg i() holds (C[x] implies p.x = F(x)) & (not
C[x] implies p.x = G(x)) from FUNCT_2:sch 5(A2);
A4: dom p = Seg i() by FUNCT_2:def 1;
then reconsider p as FinSequence by FINSEQ_1:def 2;
rng p c= D() by RELAT_1:def 19;
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
i() is Element of NAT by ORDINAL1:def 12;
hence thesis by A3,A4,FINSEQ_1:def 3;
end;
begin :: Components
definition
let X be set;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN;
func MergeSequence(p,q) -> FinSequence of bool X means
:Def1:
len it = len p
& for i be Nat st i in dom p holds it.i = IFEQ(q.i,TRUE,p.i,X\p.i);
existence
proof
deffunc F(Nat) = IFEQ(q.$1,TRUE,p.$1,X\p.$1);
consider r be FinSequence such that
A1: len r = len p and
A2: for i be Nat st i in dom r holds r.i = F(i) from FINSEQ_1:sch 2;
rng r c= bool X
proof
let z be object;
assume z in rng r;
then consider i be Nat such that
A3: i in dom r and
A4: r.i = z by FINSEQ_2:10;
A5: z = IFEQ(q.i,TRUE,p.i,X\p.i) by A2,A3,A4;
i in Seg len p by A1,A3,FINSEQ_1:def 3;
then
A6: i in dom p by FINSEQ_1:def 3;
now
per cases;
suppose
q.i = TRUE;
then z = p.i by A5,FUNCOP_1:def 8;
hence thesis by A6,FINSEQ_2:11;
end;
suppose
q.i <> TRUE;
then z = X\p.i by A5,FUNCOP_1:def 8;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider r as FinSequence of bool X by FINSEQ_1:def 4;
take r;
dom p = dom r by A1,FINSEQ_3:29;
hence thesis by A1,A2;
end;
uniqueness
proof
let r1,r2 be FinSequence of bool X such that
A7: len r1 = len p and
A8: for i be Nat st i in dom p holds r1.i = IFEQ(q.i,TRUE,p.i,X\p.i) and
A9: len r2 = len p and
A10: for i be Nat st i in dom p holds r2.i = IFEQ(q.i,TRUE,p.i,X\p.i);
A11: dom r1 = Seg len p by A7,FINSEQ_1:def 3;
now
let i be Nat;
assume i in dom r1;
then
A12: i in dom p by A11,FINSEQ_1:def 3;
hence r1.i = IFEQ(q.i,TRUE,p.i,X\p.i) by A8
.= r2.i by A10,A12;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
::$CT 3
theorem Th1:
for X be set for p be FinSequence of bool X for q be FinSequence
of BOOLEAN holds dom MergeSequence(p,q) = dom p
proof
let X be set;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN;
thus dom MergeSequence(p,q) = Seg len MergeSequence(p,q) by FINSEQ_1:def 3
.= Seg len p by Def1
.= dom p by FINSEQ_1:def 3;
end;
theorem Th2:
for X be set for p be FinSequence of bool X for q be FinSequence
of BOOLEAN for i be Nat st q.i = TRUE holds MergeSequence(p,q).i = p.i
proof
let X be set;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN;
let i be Nat;
assume
A1: q.i = TRUE;
now
per cases;
suppose
i in dom p;
hence MergeSequence(p,q).i = IFEQ(q.i,TRUE,p.i,X\p.i) by Def1
.= p.i by A1,FUNCOP_1:def 8;
end;
suppose
A2: not i in dom p;
dom p = Seg len p by FINSEQ_1:def 3
.= Seg len MergeSequence(p,q) by Def1
.= dom MergeSequence(p,q) by FINSEQ_1:def 3;
hence MergeSequence(p,q).i = {} by A2,FUNCT_1:def 2
.= p.i by A2,FUNCT_1:def 2;
end;
end;
hence thesis;
end;
theorem Th3:
for X be set for p be FinSequence of bool X for q be FinSequence
of BOOLEAN for i be Nat st i in dom p & q.i = FALSE holds MergeSequence(p,q).i
= X\p.i
proof
let X be set;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN;
let i be Nat;
assume that
A1: i in dom p and
A2: q.i = FALSE;
thus MergeSequence(p,q).i = IFEQ(q.i,TRUE,p.i,X\p.i) by A1,Def1
.= X\p.i by A2,FUNCOP_1:def 8;
end;
theorem
for X be set for q be FinSequence of BOOLEAN holds len MergeSequence(
<*>(bool X),q) = 0
proof
let X be set;
let q be FinSequence of BOOLEAN;
thus len MergeSequence(<*>(bool X),q) = len <*>(bool X) by Def1
.= 0;
end;
theorem Th5:
for X be set for q be FinSequence of BOOLEAN holds MergeSequence(
<*>(bool X),q) = <*>(bool X)
proof
let X be set;
let q be FinSequence of BOOLEAN;
len MergeSequence(<*>(bool X),q) = len <*>(bool X) by Def1
.= 0;
hence thesis;
end;
theorem
for X be set for x be Subset of X for q be FinSequence of BOOLEAN
holds len MergeSequence(<*x*>,q) = 1
proof
let X be set;
let x be Subset of X;
let q be FinSequence of BOOLEAN;
thus len MergeSequence(<*x*>,q) = len <*x*> by Def1
.= 1 by FINSEQ_1:39;
end;
theorem
for X be set for x be Subset of X for q be FinSequence of BOOLEAN
holds (q.1 = TRUE implies MergeSequence(<*x*>,q).1 = x) & (q.1 = FALSE implies
MergeSequence(<*x*>,q).1 = X\x)
proof
let X be set;
let x be Subset of X;
let q be FinSequence of BOOLEAN;
thus q.1 = TRUE implies MergeSequence(<*x*>,q).1 = x
proof
assume q.1 = TRUE;
hence MergeSequence(<*x*>,q).1 = <*x*>.1 by Th2
.= x;
end;
1 in Seg 1 by FINSEQ_1:1;
then
A1: 1 in dom <*x*> by FINSEQ_1:38;
assume q.1 = FALSE;
hence MergeSequence(<*x*>,q).1 = X\<*x*>.1 by A1,Th3
.= X\x;
end;
theorem
for X be set for x,y be Subset of X for q be FinSequence of BOOLEAN
holds len MergeSequence(<*x,y*>,q) = 2
proof
let X be set;
let x,y be Subset of X;
let q be FinSequence of BOOLEAN;
thus len MergeSequence(<*x,y*>,q) = len <*x,y*> by Def1
.= 2 by FINSEQ_1:44;
end;
theorem
for X be set for x,y be Subset of X for q be FinSequence of BOOLEAN
holds (q.1 = TRUE implies MergeSequence(<*x,y*>,q).1 = x) & (q.1 = FALSE
implies MergeSequence(<*x,y*>,q).1 = X\x) & (q.2 = TRUE implies MergeSequence(
<*x,y*>,q).2 = y) & (q.2 = FALSE implies MergeSequence(<*x,y*>,q).2 = X\y)
proof
let X be set;
let x,y be Subset of X;
let q be FinSequence of BOOLEAN;
thus q.1 = TRUE implies MergeSequence(<*x,y*>,q).1 = x
proof
assume q.1 = TRUE;
hence MergeSequence(<*x,y*>,q).1 = <*x,y*>.1 by Th2
.= x;
end;
2 in Seg 2 by FINSEQ_1:1;
then
A1: 2 in dom <*x,y*> by FINSEQ_1:89;
1 in Seg 2 by FINSEQ_1:1;
then
A2: 1 in dom <*x,y*> by FINSEQ_1:89;
thus q.1 = FALSE implies MergeSequence(<*x,y*>,q).1 = X\x
proof
assume q.1 = FALSE;
hence MergeSequence(<*x,y*>,q).1 = X\<*x,y*>.1 by A2,Th3
.= X\x;
end;
thus q.2 = TRUE implies MergeSequence(<*x,y*>,q).2 = y
proof
assume q.2 = TRUE;
hence MergeSequence(<*x,y*>,q).2 = <*x,y*>.2 by Th2
.= y;
end;
assume q.2 = FALSE;
hence MergeSequence(<*x,y*>,q).2 = X\<*x,y*>.2 by A1,Th3
.= X\y;
end;
theorem
for X be set for x,y,z be Subset of X for q be FinSequence of BOOLEAN
holds len MergeSequence(<*x,y,z*>,q) = 3
proof
let X be set;
let x,y,z be Subset of X;
let q be FinSequence of BOOLEAN;
thus len MergeSequence(<*x,y,z*>,q) = len <*x,y,z*> by Def1
.= 3 by FINSEQ_1:45;
end;
theorem
for X be set for x,y,z be Subset of X for q be FinSequence of BOOLEAN
holds (q.1 = TRUE implies MergeSequence(<*x,y,z*>,q).1 = x) & (q.1 = FALSE
implies MergeSequence(<*x,y,z*>,q).1 = X\x) & (q.2 = TRUE implies MergeSequence
(<*x,y,z*>,q).2 = y) & (q.2 = FALSE implies MergeSequence(<*x,y,z*>,q).2 = X\y)
& (q.3 = TRUE implies MergeSequence(<*x,y,z*>,q).3 = z) & (q.3 = FALSE implies
MergeSequence(<*x,y,z*>,q).3 = X\z)
proof
let X be set;
let x,y,z be Subset of X;
let q be FinSequence of BOOLEAN;
thus q.1 = TRUE implies MergeSequence(<*x,y,z*>,q).1 = x
proof
assume q.1 = TRUE;
hence MergeSequence(<*x,y,z*>,q).1 = <*x,y,z*>.1 by Th2
.= x;
end;
3 in Seg 3 by FINSEQ_1:1;
then
A1: 3 in dom <*x,y,z*> by FINSEQ_1:89;
1 in Seg 3 by FINSEQ_1:1;
then
A2: 1 in dom <*x,y,z*> by FINSEQ_1:89;
thus q.1 = FALSE implies MergeSequence(<*x,y,z*>,q).1 = X\x
proof
assume q.1 = FALSE;
hence MergeSequence(<*x,y,z*>,q).1 = X\<*x,y,z*>.1 by A2,Th3
.= X\x;
end;
thus q.2 = TRUE implies MergeSequence(<*x,y,z*>,q).2 = y
proof
assume q.2 = TRUE;
hence MergeSequence(<*x,y,z*>,q).2 = <*x,y,z*>.2 by Th2
.= y;
end;
2 in Seg 3 by FINSEQ_1:1;
then
A3: 2 in dom <*x,y,z*> by FINSEQ_1:89;
thus q.2 = FALSE implies MergeSequence(<*x,y,z*>,q).2 = X\y
proof
assume q.2 = FALSE;
hence MergeSequence(<*x,y,z*>,q).2 = X\<*x,y,z*>.2 by A3,Th3
.= X\y;
end;
thus q.3 = TRUE implies MergeSequence(<*x,y,z*>,q).3 = z
proof
assume q.3 = TRUE;
hence MergeSequence(<*x,y,z*>,q).3 = <*x,y,z*>.3 by Th2
.= z;
end;
assume q.3 = FALSE;
hence MergeSequence(<*x,y,z*>,q).3 = X\<*x,y,z*>.3 by A1,Th3
.= X\z;
end;
theorem Th12:
for X be set for p be FinSequence of bool X holds { Intersect (
rng MergeSequence(p,q)) where q is FinSequence of BOOLEAN : len q = len p } is
Subset-Family of X
proof
let X be set;
let p be FinSequence of bool X;
{ Intersect (rng MergeSequence(p,q)) where q is FinSequence of BOOLEAN :
len q = len p } c= bool X
proof
let z be object;
assume z in { Intersect (rng MergeSequence(p,q)) where q is FinSequence
of BOOLEAN : len q = len p };
then
ex q be FinSequence of BOOLEAN st z = Intersect (rng MergeSequence(p,q)
) & len q = len p;
hence thesis;
end;
hence thesis;
end;
registration
cluster -> boolean-valued for FinSequence of BOOLEAN;
coherence
proof
let f be FinSequence of BOOLEAN;
thus rng f c= BOOLEAN;
end;
end;
definition
let X be set;
let Y be finite Subset-Family of X;
func Components(Y) -> Subset-Family of X means
:Def2:
ex p be FinSequence of
bool X st len p = card Y & rng p = Y & it = { Intersect (rng MergeSequence(p,q)
) where q is FinSequence of BOOLEAN : len q = len p };
existence
proof
consider p be FinSequence such that
A1: rng p = Y and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of bool X by A1,FINSEQ_1:def 4;
reconsider C = { Intersect (rng MergeSequence(p,q)) where q is FinSequence
of BOOLEAN : len q = len p } as Subset-Family of X by Th12;
take C,p;
thus thesis by A1,A2,FINSEQ_4:62;
end;
uniqueness
proof
let C1,C2 be Subset-Family of X such that
A3: ex p be FinSequence of bool X st len p = card Y & rng p = Y & C1 =
{ Intersect (rng MergeSequence(p,q)) where q is FinSequence of BOOLEAN : len q
= len p } and
A4: ex p be FinSequence of bool X st len p = card Y & rng p = Y & C2 =
{ Intersect (rng MergeSequence(p,q)) where q is FinSequence of BOOLEAN : len q
= len p };
consider p1 be FinSequence of bool X such that
A5: len p1 = card Y and
A6: rng p1 = Y and
A7: C1 = { Intersect (rng MergeSequence(p1,q)) where q is FinSequence
of BOOLEAN : len q = len p1 } by A3;
consider p2 be FinSequence of bool X such that
A8: len p2 = card Y and
A9: rng p2 = Y and
A10: C2 = { Intersect (rng MergeSequence(p2,q)) where q is FinSequence
of BOOLEAN : len q = len p2 } by A4;
A11: p2 is one-to-one by A8,A9,FINSEQ_4:62;
A12: p1 is one-to-one by A5,A6,FINSEQ_4:62;
now
let P be Subset of X;
thus P in C1 implies P in C2
proof
p1 is Function of dom p1,rng p1 by FUNCT_2:1;
then
A13: p1" is Function of rng p1,dom p1 by A12,FUNCT_2:25;
p2 is FinSequence of rng p1 by A6,A9,FINSEQ_1:def 4;
then
A14: p1"*p2 is FinSequence of dom p1 by A13,FINSEQ_2:32;
assume P in C1;
then consider q be FinSequence of BOOLEAN such that
A15: P = Intersect (rng MergeSequence(p1,q)) and
A16: len q = len p1 by A7;
A17: dom p1 = Seg len q by A16,FINSEQ_1:def 3
.= dom q by FINSEQ_1:def 3;
then q is Function of dom p1,BOOLEAN by FINSEQ_2:26;
then q*(p1"*p2) is FinSequence of BOOLEAN by A14,FINSEQ_2:32;
then reconsider q1 = q*p1"*p2 as FinSequence of BOOLEAN by RELAT_1:36;
A18: rng p2 = dom (p1") by A6,A9,A12,FUNCT_1:33;
then
A19: dom (p1"*p2) = dom p2 by RELAT_1:27;
rng (p1"*p2) = rng (p1") by A18,RELAT_1:28
.= dom q by A12,A17,FUNCT_1:33;
then
A20: dom (q*(p1"*p2)) = dom p2 by A19,RELAT_1:27;
A21: rng p1 = dom (p2") by A6,A9,A11,FUNCT_1:33;
then
A22: dom (p2"*p1) = dom p1 by RELAT_1:27;
A23: Seg len q1 = dom q1 by FINSEQ_1:def 3
.= dom p2 by A20,RELAT_1:36
.= Seg len p2 by FINSEQ_1:def 3;
then
A24: dom p2 = Seg len q1 by FINSEQ_1:def 3
.= dom q1 by FINSEQ_1:def 3;
rng (p2"*p1) = rng (p2") by A21,RELAT_1:28
.= dom q1 by A11,A24,FUNCT_1:33;
then
A25: dom (q1*(p2"*p1)) = dom p1 by A22,RELAT_1:27;
A26: q1*p2"*p1 = q*p1"*p2*(p2"*p1) by RELAT_1:36
.= q*p1"*(p2*(p2"*p1)) by RELAT_1:36
.= q*p1"*(p2*p2"*p1) by RELAT_1:36
.= q*p1"*((id rng p2)*p1) by A11,FUNCT_1:39
.= q*p1"*p1 by A6,A9,RELAT_1:54
.= q*(p1"*p1) by RELAT_1:36
.= q*(id dom p1) by A12,FUNCT_1:39
.= q by A17,RELAT_1:52;
A27: rng MergeSequence(p1,q) c= rng MergeSequence(p2,q1)
proof
let z be object;
assume z in rng MergeSequence(p1,q);
then consider j be Nat such that
A28: j in dom MergeSequence(p1,q) and
A29: MergeSequence(p1,q).j = z by FINSEQ_2:10;
j in Seg len MergeSequence(p1,q) by A28,FINSEQ_1:def 3;
then
A30: j in Seg len p1 by Def1;
then
A31: j in dom (q1*(p2"*p1)) by A25,FINSEQ_1:def 3;
A32: j in dom p1 by A30,FINSEQ_1:def 3;
then
A33: j in dom (p2"*p1) by A21,RELAT_1:27;
then (p2"*p1).j in rng (p2"*p1) by FUNCT_1:def 3;
then (p2"*p1).j in rng (p2") by FUNCT_1:14;
then
A34: (p2"*p1).j in dom p2 by A11,FUNCT_1:33;
then reconsider pj = (p2"*p1).j as Element of NAT;
A35: q.j = (q1*(p2"*p1)).j by A26,RELAT_1:36
.= q1.((p2"*p1).j) by A31,FUNCT_1:12;
A36: now
per cases by XBOOLEAN:def 3;
suppose
A37: q.j = TRUE;
hence MergeSequence(p2,q1).((p2"*p1).j) = p2.pj by A35,Th2
.= (p2*(p2"*p1)).j by A33,FUNCT_1:13
.= (p2*p2"*p1).j by RELAT_1:36
.= (id(rng p1)*p1).j by A6,A9,A11,FUNCT_1:39
.= p1.j by RELAT_1:54
.= z by A29,A37,Th2;
end;
suppose
A38: q.j = FALSE;
hence MergeSequence(p2,q1).((p2"*p1).j) = X\p2.pj
by A34,A35,Th3
.= X\(p2*(p2"*p1)).j by A33,FUNCT_1:13
.= X\(p2*p2"*p1).j by RELAT_1:36
.= X\(id(rng p1)*p1).j by A6,A9,A11,FUNCT_1:39
.= X\p1.j by RELAT_1:54
.= z by A29,A32,Th3,A38;
end;
end;
(p2"*p1).j in Seg len p2 by A34,FINSEQ_1:def 3;
then (p2"*p1).j in Seg len MergeSequence(p2,q1) by Def1;
then (p2"*p1).j in dom MergeSequence(p2,q1) by FINSEQ_1:def 3;
hence thesis by A36,FUNCT_1:def 3;
end;
A39: len q1 = len p2 by A23,FINSEQ_1:6;
rng MergeSequence(p2,q1) c= rng MergeSequence(p1,q)
proof
let z be object;
assume z in rng MergeSequence(p2,q1);
then consider j be Nat such that
A40: j in dom MergeSequence(p2,q1) and
A41: MergeSequence(p2,q1).j = z by FINSEQ_2:10;
j in Seg len MergeSequence(p2,q1) by A40,FINSEQ_1:def 3;
then
A42: j in Seg len p2 by Def1;
then
A43: j in dom (q*(p1"*p2)) by A20,FINSEQ_1:def 3;
A44: j in dom p2 by A42,FINSEQ_1:def 3;
then
A45: j in dom (p1"*p2) by A18,RELAT_1:27;
then (p1"*p2).j in rng (p1"*p2) by FUNCT_1:def 3;
then (p1"*p2).j in rng (p1") by FUNCT_1:14;
then
A46: (p1"*p2).j in dom p1 by A12,FUNCT_1:33;
then reconsider pj = (p1"*p2).j as Element of NAT;
A47: q1.j = (q*(p1"*p2)).j by RELAT_1:36
.= q.((p1"*p2).j) by A43,FUNCT_1:12;
A48: now
per cases by XBOOLEAN:def 3;
suppose
A49: q1.j = TRUE;
hence MergeSequence(p1,q).((p1"*p2).j) = p1.pj by A47,Th2
.= (p1*(p1"*p2)).j by A45,FUNCT_1:13
.= (p1*p1"*p2).j by RELAT_1:36
.= (id(rng p2)*p2).j by A6,A9,A12,FUNCT_1:39
.= p2.j by RELAT_1:54
.= z by A41,A49,Th2;
end;
suppose
A50: q1.j = FALSE;
hence MergeSequence(p1,q).((p1"*p2).j) = X\p1.pj by A46,A47,Th3
.= X\(p1*(p1"*p2)).j by A45,FUNCT_1:13
.= X\(p1*p1"*p2).j by RELAT_1:36
.= X\(id(rng p2)*p2).j by A6,A9,A12,FUNCT_1:39
.= X\p2.j by RELAT_1:54
.= z by A41,A44,A50,Th3;
end;
end;
(p1"*p2).j in Seg len p1 by A46,FINSEQ_1:def 3;
then (p1"*p2).j in Seg len MergeSequence(p1,q) by Def1;
then (p1"*p2).j in dom MergeSequence(p1,q) by FINSEQ_1:def 3;
hence thesis by A48,FUNCT_1:def 3;
end;
then P = Intersect (rng MergeSequence(p2,q1)) by A15,A27,
XBOOLE_0:def 10;
hence thesis by A10,A39;
end;
thus P in C2 implies P in C1
proof
p2 is Function of dom p2,rng p2 by FUNCT_2:1;
then
A51: p2" is Function of rng p2,dom p2 by A11,FUNCT_2:25;
p1 is FinSequence of rng p2 by A6,A9,FINSEQ_1:def 4;
then
A52: p2"*p1 is FinSequence of dom p2 by A51,FINSEQ_2:32;
assume P in C2;
then consider q be FinSequence of BOOLEAN such that
A53: P = Intersect (rng MergeSequence(p2,q)) and
A54: len q = len p2 by A10;
A55: dom p2 = Seg len q by A54,FINSEQ_1:def 3
.= dom q by FINSEQ_1:def 3;
then q is Function of dom p2,BOOLEAN by FINSEQ_2:26;
then q*(p2"*p1) is FinSequence of BOOLEAN by A52,FINSEQ_2:32;
then reconsider q1 = q*p2"*p1 as FinSequence of BOOLEAN by RELAT_1:36;
A56: rng p1 = dom (p2") by A6,A9,A11,FUNCT_1:33;
then
A57: dom (p2"*p1) = dom p1 by RELAT_1:27;
rng (p2"*p1) = rng (p2") by A56,RELAT_1:28
.= dom q by A11,A55,FUNCT_1:33;
then
A58: dom (q*(p2"*p1)) = dom p1 by A57,RELAT_1:27;
A59: rng p2 = dom (p1") by A6,A9,A12,FUNCT_1:33;
then
A60: dom (p1"*p2) = dom p2 by RELAT_1:27;
A61: Seg len q1 = dom q1 by FINSEQ_1:def 3
.= dom p1 by A58,RELAT_1:36
.= Seg len p1 by FINSEQ_1:def 3;
then
A62: dom p1 = Seg len q1 by FINSEQ_1:def 3
.= dom q1 by FINSEQ_1:def 3;
rng (p1"*p2) = rng (p1") by A59,RELAT_1:28
.= dom q1 by A12,A62,FUNCT_1:33;
then
A63: dom (q1*(p1"*p2)) = dom p2 by A60,RELAT_1:27;
A64: q1*p1"*p2 = q*p2"*p1*(p1"*p2) by RELAT_1:36
.= q*p2"*(p1*(p1"*p2)) by RELAT_1:36
.= q*p2"*(p1*p1"*p2) by RELAT_1:36
.= q*p2"*((id rng p1)*p2) by A12,FUNCT_1:39
.= q*p2"*p2 by A6,A9,RELAT_1:54
.= q*(p2"*p2) by RELAT_1:36
.= q*(id dom p2) by A11,FUNCT_1:39
.= q by A55,RELAT_1:52;
A65: rng MergeSequence(p2,q) c= rng MergeSequence(p1,q1)
proof
let z be object;
assume z in rng MergeSequence(p2,q);
then consider j be Nat such that
A66: j in dom MergeSequence(p2,q) and
A67: MergeSequence(p2,q).j = z by FINSEQ_2:10;
j in Seg len MergeSequence(p2,q) by A66,FINSEQ_1:def 3;
then
A68: j in Seg len p2 by Def1;
then
A69: j in dom (q1*(p1"*p2)) by A63,FINSEQ_1:def 3;
A70: j in dom p2 by A68,FINSEQ_1:def 3;
then
A71: j in dom (p1"*p2) by A59,RELAT_1:27;
then (p1"*p2).j in rng (p1"*p2) by FUNCT_1:def 3;
then (p1"*p2).j in rng (p1") by FUNCT_1:14;
then
A72: (p1"*p2).j in dom p1 by A12,FUNCT_1:33;
then reconsider pj = (p1"*p2).j as Element of NAT;
A73: q.j = (q1*(p1"*p2)).j by A64,RELAT_1:36
.= q1.((p1"*p2).j) by A69,FUNCT_1:12;
A74: now
per cases by XBOOLEAN:def 3;
suppose
A75: q.j = TRUE;
hence MergeSequence(p1,q1).((p1"*p2).j) = p1.pj by A73,Th2
.= (p1*(p1"*p2)).j by A71,FUNCT_1:13
.= (p1*p1"*p2).j by RELAT_1:36
.= (id(rng p2)*p2).j by A6,A9,A12,FUNCT_1:39
.= p2.j by RELAT_1:54
.= z by A67,A75,Th2;
end;
suppose
A76: q.j = FALSE;
hence MergeSequence(p1,q1).((p1"*p2).j) = X\p1.pj by A72,A73,Th3
.= X\(p1*(p1"*p2)).j by A71,FUNCT_1:13
.= X\(p1*p1"*p2).j by RELAT_1:36
.= X\(id(rng p2)*p2).j by A6,A9,A12,FUNCT_1:39
.= X\p2.j by RELAT_1:54
.= z by A67,A70,A76,Th3;
end;
end;
(p1"*p2).j in Seg len p1 by A72,FINSEQ_1:def 3;
then (p1"*p2).j in Seg len MergeSequence(p1,q1) by Def1;
then (p1"*p2).j in dom MergeSequence(p1,q1) by FINSEQ_1:def 3;
hence thesis by A74,FUNCT_1:def 3;
end;
A77: len q1 = len p1 by A61,FINSEQ_1:6;
rng MergeSequence(p1,q1) c= rng MergeSequence(p2,q)
proof
let z be object;
assume z in rng MergeSequence(p1,q1);
then consider j be Nat such that
A78: j in dom MergeSequence(p1,q1) and
A79: MergeSequence(p1,q1).j = z by FINSEQ_2:10;
j in Seg len MergeSequence(p1,q1) by A78,FINSEQ_1:def 3;
then
A80: j in Seg len p1 by Def1;
then
A81: j in dom (q*(p2"*p1)) by A58,FINSEQ_1:def 3;
A82: j in dom p1 by A80,FINSEQ_1:def 3;
then
A83: j in dom (p2"*p1) by A56,RELAT_1:27;
then (p2"*p1).j in rng (p2"*p1) by FUNCT_1:def 3;
then (p2"*p1).j in rng (p2") by FUNCT_1:14;
then
A84: (p2"*p1).j in dom p2 by A11,FUNCT_1:33;
then reconsider pj = (p2"*p1).j as Element of NAT;
A85: q1.j = (q*(p2"*p1)).j by RELAT_1:36
.= q.((p2"*p1).j) by A81,FUNCT_1:12;
A86: now
per cases by XBOOLEAN:def 3;
suppose
A87: q1.j = TRUE;
hence MergeSequence(p2,q).((p2"*p1).j) = p2.pj by A85,Th2
.= (p2*(p2"*p1)).j by A83,FUNCT_1:13
.= (p2*p2"*p1).j by RELAT_1:36
.= (id(rng p1)*p1).j by A6,A9,A11,FUNCT_1:39
.= p1.j by RELAT_1:54
.= z by A79,A87,Th2;
end;
suppose
A88: q1.j = FALSE;
hence MergeSequence(p2,q).((p2"*p1).j) = X\p2.pj by A84,A85,Th3
.= X\(p2*(p2"*p1)).j by A83,FUNCT_1:13
.= X\(p2*p2"*p1).j by RELAT_1:36
.= X\(id(rng p1)*p1).j by A6,A9,A11,FUNCT_1:39
.= X\p1.j by RELAT_1:54
.= z by A79,A82,A88,Th3;
end;
end;
(p2"*p1).j in Seg len p2 by A84,FINSEQ_1:def 3;
then (p2"*p1).j in Seg len MergeSequence(p2,q) by Def1;
then (p2"*p1).j in dom MergeSequence(p2,q) by FINSEQ_1:def 3;
hence thesis by A86,FUNCT_1:def 3;
end;
then P = Intersect (rng MergeSequence(p1,q1)) by A53,A65,
XBOOLE_0:def 10;
hence thesis by A7,A77;
end;
end;
hence thesis by SETFAM_1:31;
end;
end;
registration
let X be set;
let Y be finite Subset-Family of X;
cluster Components(Y) -> finite;
coherence
proof
consider p be FinSequence of bool X such that
len p = card Y and
rng p = Y and
A1: Components(Y) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
deffunc F(Element of BOOLEAN*) = Intersect (rng MergeSequence(p,$1));
A2: Components(Y) c= { Intersect (rng MergeSequence(p,q)) where q is
Element of BOOLEAN* : q in len p-tuples_on BOOLEAN }
proof
let z be object;
assume z in Components(Y);
then consider q be FinSequence of BOOLEAN such that
A3: z = Intersect (rng MergeSequence(p,q)) & len q = len p by A1;
q is Element of BOOLEAN* & q is Element of len q-tuples_on BOOLEAN
by FINSEQ_1:def 11,FINSEQ_2:92;
hence thesis by A3;
end;
A4: len p-tuples_on BOOLEAN is finite;
{ F(q) where q is Element of BOOLEAN* : q in len p-tuples_on BOOLEAN }
is finite from FRAENKEL:sch 21(A4);
hence thesis by A2;
end;
end;
theorem Th13:
for X be set for Y be empty Subset-Family of X holds Components( Y) = {X}
proof
let X be set;
let Y be empty Subset-Family of X;
consider p be FinSequence of bool X such that
A1: len p = card Y and
A2: rng p = Y and
A3: Components(Y) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
thus Components(Y) = {X}
proof
thus Components(Y) c= {X}
proof
let z be object;
assume z in Components(Y);
then consider q be FinSequence of BOOLEAN such that
A4: z = Intersect (rng MergeSequence(p,q)) and
len q = len p by A3;
p = <*>(bool X) by A2;
then rng MergeSequence(p,q) = {} by Th5,RELAT_1:38;
then Intersect (rng MergeSequence(p,q)) = X by SETFAM_1:def 9;
hence thesis by A4,TARSKI:def 1;
end;
let z be object;
p = <*>(bool X) by A2;
then rng MergeSequence(p,<*>(BOOLEAN)) = {} by Th5,RELAT_1:38;
then
A5: Intersect (rng MergeSequence(p,<*>(BOOLEAN))) = X by SETFAM_1:def 9;
assume z in {X};
then z = X by TARSKI:def 1;
hence thesis by A1,A3,A5;
end;
end;
theorem
for X be set for Y,Z be finite Subset-Family of X st Z c= Y holds
Components(Y) is_finer_than Components(Z)
proof
let X be set;
let Y,Z be finite Subset-Family of X;
assume
A1: Z c= Y;
now
let V be set;
consider p be FinSequence of bool X such that
A2: len p = card Y and
A3: rng p = Y and
A4: Components(Y) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
consider p1 be FinSequence of bool X such that
len p1 = card Z and
A5: rng p1 = Z and
A6: Components(Z) = { Intersect (rng MergeSequence(p1,q)) where q is
FinSequence of BOOLEAN : len q = len p1 } by Def2;
A7: p1 is FinSequence of rng p by A1,A3,A5,FINSEQ_1:def 4;
assume V in Components(Y);
then consider q be FinSequence of BOOLEAN such that
A8: V = Intersect (rng MergeSequence(p,q)) and
A9: len q = len p by A4;
dom p = dom q by A9,FINSEQ_3:29;
then
A10: q is Function of dom p,BOOLEAN by FINSEQ_2:26;
A11: p is one-to-one by A2,A3,FINSEQ_4:62;
then
A12: rng p1 c= dom (p") by A1,A3,A5,FUNCT_1:33;
rng (p") = dom p by A11,FUNCT_1:33
.= dom q by A9,FINSEQ_3:29;
then
A13: rng (p"*p1) c= dom q by RELAT_1:26;
p is Function of dom p,rng p by FUNCT_2:1;
then p" is Function of rng p,dom p by A11,FUNCT_2:25;
then p"*p1 is FinSequence of dom p by A7,FINSEQ_2:32;
then q*(p"*p1) is FinSequence of BOOLEAN by A10,FINSEQ_2:32;
then reconsider q1 = q*p"*p1 as FinSequence of BOOLEAN by RELAT_1:36;
reconsider W = Intersect (rng MergeSequence(p1,q1)) as set;
take W;
dom q1 = dom (q*(p"*p1)) by RELAT_1:36
.= dom (p"*p1) by A13,RELAT_1:27
.= dom p1 by A12,RELAT_1:27;
then len q1 = len p1 by FINSEQ_3:29;
hence W in Components(Z) by A6;
rng MergeSequence(p1,q1) c= rng MergeSequence(p,q)
proof
let z be object;
assume z in rng MergeSequence(p1,q1);
then consider i be Nat such that
A14: i in dom MergeSequence(p1,q1) and
A15: MergeSequence(p1,q1).i = z by FINSEQ_2:10;
A16: i in dom p1 by A14,Th1;
then
A17: i in dom (p"*p1) by A12,RELAT_1:27;
then (p"*p1).i in rng (p"*p1) by FUNCT_1:def 3;
then
A18: (p"*p1).i in rng (p") by FUNCT_1:14;
then
A19: (p"*p1).i in dom p by A11,FUNCT_1:33;
then reconsider j = (p"*p1).i as Element of NAT;
A20: q.j = (q*(p"*p1)).i by A17,FUNCT_1:13
.= q1.i by RELAT_1:36;
A21: p1 is Function of dom p1,rng p by A1,A3,A5,FUNCT_2:2;
A22: j in dom p by A11,A18,FUNCT_1:33;
A23: now
per cases by XBOOLEAN:def 3;
suppose
A24: q.j = TRUE;
hence MergeSequence(p,q).j = p.j by Th2
.= (p*(p"*p1)).i by A17,FUNCT_1:13
.= (p*p"*p1).i by RELAT_1:36
.= ((id rng p)*p1).i by A11,FUNCT_1:39
.= p1.i by A21,FUNCT_2:17
.= z by A15,A20,A24,Th2;
end;
suppose
A25: q.j = FALSE;
hence MergeSequence(p,q).j = X\p.j by A22,Th3
.= X\(p*(p"*p1)).i by A17,FUNCT_1:13
.= X\(p*p"*p1).i by RELAT_1:36
.= X\((id rng p)*p1).i by A11,FUNCT_1:39
.= X\p1.i by A21,FUNCT_2:17
.= z by A15,A16,A20,A25,Th3;
end;
end;
j in dom MergeSequence(p,q) by A19,Th1;
hence thesis by A23,FUNCT_1:def 3;
end;
hence V c= W by A8,SETFAM_1:44;
end;
hence thesis by SETFAM_1:def 2;
end;
theorem Th15:
for X be set for Y be finite Subset-Family of X holds union Components(Y) = X
proof
let X be set;
let Y be finite Subset-Family of X;
X c= union Components(Y)
proof
deffunc F(set) = FALSE;
deffunc T(set) = TRUE;
let z be object;
consider p be FinSequence of bool X such that
len p = card Y and
rng p = Y and
A1: Components(Y) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
defpred C[set] means z in p.$1;
A2: for i be Nat st i in Seg len p holds (C[i] implies T(i) in BOOLEAN) &
(not C[i] implies F(i) in BOOLEAN);
consider q be FinSequence of BOOLEAN such that
A3: len q = len p and
A4: for i be Nat st i in Seg len p holds (C[i] implies q.i = T(i)) & (
not C[i] implies q.i = F(i)) from SeqLambda1C(A2);
assume
A5: z in X;
now
let Z be set;
assume Z in rng MergeSequence(p,q);
then consider i be Nat such that
A6: i in dom MergeSequence(p,q) and
A7: MergeSequence(p,q).i = Z by FINSEQ_2:10;
A8: dom MergeSequence(p,q) = dom p by Th1;
then
A9: dom MergeSequence(p,q) = Seg len p by FINSEQ_1:def 3;
now
per cases;
suppose
A10: z in p.i;
then q.i = TRUE by A4,A6,A9;
hence z in Z by A7,A10,Th2;
end;
suppose
A11: not z in p.i;
then q.i = FALSE by A4,A6,A9;
then MergeSequence(p,q).i = X\p.i by A6,A8,Th3;
hence z in Z by A5,A7,A11,XBOOLE_0:def 5;
end;
end;
hence z in Z;
end;
then
A12: z in Intersect (rng MergeSequence(p,q)) by A5,SETFAM_1:43;
Intersect (rng MergeSequence(p,q)) in Components(Y) by A1,A3;
hence thesis by A12,TARSKI:def 4;
end;
hence thesis;
end;
theorem Th16:
for X be set for Y be finite Subset-Family of X for A,B be set
st A in Components(Y) & B in Components(Y) & A <> B holds A misses B
proof
let X be set;
let Y be finite Subset-Family of X;
let A,B be set;
assume that
A1: A in Components(Y) and
A2: B in Components(Y) and
A3: A <> B;
assume A /\ B <> {};
then consider z be object such that
A4: z in A /\ B by XBOOLE_0:def 1;
A5: z in B by A4,XBOOLE_0:def 4;
A6: z in A by A4,XBOOLE_0:def 4;
consider p be FinSequence of bool X such that
len p = card Y and
rng p = Y and
A7: Components(Y) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
consider q1 be FinSequence of BOOLEAN such that
A8: A = Intersect (rng MergeSequence(p,q1)) and
len q1 = len p by A1,A7;
consider q2 be FinSequence of BOOLEAN such that
A9: B = Intersect (rng MergeSequence(p,q2)) and
len q2 = len p by A2,A7;
A10: len MergeSequence(p,q1) = len p by Def1;
then
A11: dom MergeSequence(p,q1) = Seg len p by FINSEQ_1:def 3;
A12: now
let i be Nat;
assume
A13: i in dom MergeSequence(p,q1);
then
A14: i in dom p by A11,FINSEQ_1:def 3;
MergeSequence(p,q1).i in rng MergeSequence(p,q1) by A13,FUNCT_1:def 3;
then
A15: z in MergeSequence(p,q1).i by A8,A6,SETFAM_1:43;
i in dom MergeSequence(p,q2) by A14,Th1;
then MergeSequence(p,q2).i in rng MergeSequence(p,q2) by FUNCT_1:def 3;
then
A16: z in MergeSequence(p,q2).i by A9,A5,SETFAM_1:43;
per cases by XBOOLEAN:def 3;
suppose
q1.i = TRUE;
then
A17: MergeSequence(p,q1).i = p.i by Th2;
q2.i = TRUE
proof
assume not q2.i = TRUE;
then MergeSequence(p,q2).i = X\p.i by A14,Th3,XBOOLEAN:def 3;
hence contradiction by A15,A16,A17,XBOOLE_0:def 5;
end;
hence MergeSequence(p,q1).i = MergeSequence(p,q2).i by A17,Th2;
end;
suppose q1.i = FALSE;
then
A18: MergeSequence(p,q1).i = X\p.i by A14,Th3;
q2.i = FALSE
proof
assume not q2.i = FALSE;
then q2.i = TRUE by XBOOLEAN:def 3;
then MergeSequence(p,q2).i = p.i by Th2;
hence contradiction by A15,A16,A18,XBOOLE_0:def 5;
end;
hence MergeSequence(p,q1).i = MergeSequence(p,q2).i by A14,A18,Th3;
end;
end;
len MergeSequence(p,q2) = len p by Def1;
hence contradiction by A3,A8,A9,A10,A12,FINSEQ_2:9;
end;
definition
let X be set;
let Y be finite Subset-Family of X;
attr Y is in_general_position means
not {} in Components(Y);
end;
theorem
for X be set for Y,Z be finite Subset-Family of X st Z is
in_general_position & Y c= Z holds Y is in_general_position
proof
let X be set;
let Y,Z be finite Subset-Family of X such that
A1: Z is in_general_position and
A2: Y c= Z;
A3: not {} in Components(Z) by A1;
not {} in Components(Y)
proof
deffunc T(set) = TRUE;
consider p be FinSequence of bool X such that
A4: len p = card Y and
A5: rng p = Y and
A6: Components(Y) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
A7: p is one-to-one by A4,A5,FINSEQ_4:62;
then
A8: rng p = dom (p") by FUNCT_1:33;
consider p1 be FinSequence of bool X such that
A9: len p1 = card Z and
A10: rng p1 = Z and
A11: Components(Z) = { Intersect (rng MergeSequence(p1,q)) where q is
FinSequence of BOOLEAN : len q = len p1 } by Def2;
defpred C[set] means p1.$1 in rng p;
assume {} in Components(Y);
then consider q be FinSequence of BOOLEAN such that
A12: {} = Intersect (rng MergeSequence(p,q)) and
A13: len q = len p by A6;
deffunc F(set) = (q*p"*p1).$1;
A14: dom p = rng (p") by A7,FUNCT_1:33;
A15: for i be Nat st i in Seg len p1 holds (C[i] implies F(i) in BOOLEAN)
& (not C[i] implies T(i) in BOOLEAN)
proof
let i be Nat;
assume i in Seg len p1;
then
A16: i in dom p1 by FINSEQ_1:def 3;
thus p1.i in rng p implies (q*p"*p1).i in BOOLEAN
proof
assume
A17: p1.i in rng p;
rng (p") = dom q by A13,A14,FINSEQ_3:29;
then p1.i in dom (q*p") by A8,A17,RELAT_1:27;
then
A18: (q*p").(p1.i) in rng (q*p") by FUNCT_1:def 3;
dom (q*p") c= rng p by A8,RELAT_1:25;
then rng (q*p") = rng (q*p"*p1) by A2,A5,A10,RELAT_1:28,XBOOLE_1:1;
then (q*p"*p1).i in rng (q*p"*p1) by A16,A18,FUNCT_1:13;
hence thesis;
end;
thus thesis;
end;
consider q1 be FinSequence of BOOLEAN such that
A19: len q1 = len p1 and
A20: for i be Nat st i in Seg len p1 holds (C[i] implies q1.i = F(i))
& (not C[i] implies q1.i = T(i)) from SeqLambda1C(A15);
A21: p1 is one-to-one by A9,A10,FINSEQ_4:62;
then
A22: rng p1 = dom (p1") by FUNCT_1:33;
rng MergeSequence(p,q) c= rng MergeSequence(p1,q1)
proof
let z be object;
assume z in rng MergeSequence(p,q);
then consider i be Nat such that
A23: i in dom MergeSequence(p,q) and
A24: MergeSequence(p,q).i = z by FINSEQ_2:10;
i in Seg len MergeSequence(p,q) by A23,FINSEQ_1:def 3;
then i in Seg len p by Def1;
then
A25: i in dom p by FINSEQ_1:def 3;
then
A26: i in dom (p1"*p) by A2,A5,A10,A22,RELAT_1:27;
then (p1"*p).i in rng (p1"*p) by FUNCT_1:def 3;
then
A27: (p1"*p).i in rng (p1") by FUNCT_1:14;
then
A28: (p1"*p).i in dom p1 by A21,FUNCT_1:33;
then reconsider j = (p1"*p).i as Element of NAT;
p1.j = (p1*(p1"*p)).i by A26,FUNCT_1:13
.= (p1*p1"*p).i by RELAT_1:36
.= ((id rng p1)*p).i by A21,FUNCT_1:39
.= p.i by A2,A5,A10,RELAT_1:53;
then
A29: p1.j in rng p by A25,FUNCT_1:def 3;
j in Seg len p1 by A28,FINSEQ_1:def 3;
then
A30: q1.j = (q*p"*p1).((p1"*p).i) by A20,A29
.= (q*p"*p1*(p1"*p)).i by A26,FUNCT_1:13
.= (q*p"*(p1*(p1"*p))).i by RELAT_1:36
.= (q*p"*(p1*p1"*p)).i by RELAT_1:36
.= (q*p"*((id rng p1)*p)).i by A21,FUNCT_1:39
.= (q*p"*p).i by A2,A5,A10,RELAT_1:53
.= (q*(p"*p)).i by RELAT_1:36
.= (q*(id dom p)).i by A7,FUNCT_1:39
.= (q*(id dom q)).i by A13,FINSEQ_3:29
.= q.i by RELAT_1:52;
A31: j in dom p1 by A21,A27,FUNCT_1:33;
A32: now
per cases by XBOOLEAN:def 3;
suppose
A33: q.i = TRUE;
hence z = p.i by A24,Th2
.= ((id rng p1)*p).i by A2,A5,A10,RELAT_1:53
.= (p1*p1"*p).i by A21,FUNCT_1:39
.= (p1*(p1"*p)).i by RELAT_1:36
.= p1.j by A26,FUNCT_1:13
.= MergeSequence(p1,q1).j by A30,A33,Th2;
end;
suppose
A34: q.i = FALSE;
hence z = X\p.i by A24,A25,Th3
.= X\((id rng p1)*p).i by A2,A5,A10,RELAT_1:53
.= X\(p1*p1"*p).i by A21,FUNCT_1:39
.= X\(p1*(p1"*p)).i by RELAT_1:36
.= X\p1.j by A26,FUNCT_1:13
.= MergeSequence(p1,q1).j by A31,A30,A34,Th3;
end;
end;
j in dom MergeSequence(p1,q1) by A28,Th1;
hence thesis by A32,FUNCT_1:def 3;
end;
then {} = Intersect (rng MergeSequence(p1,q1)) by A12,SETFAM_1:44
,XBOOLE_1:3;
hence contradiction by A3,A11,A19;
end;
hence thesis;
end;
theorem
for X be non empty set for Y be empty Subset-Family of X holds Y is
in_general_position
proof
let X be non empty set;
let Y be empty Subset-Family of X;
not {} in {X} by TARSKI:def 1;
then not {} in Components(Y) by Th13;
hence thesis;
end;
theorem
for X be non empty set for Y be finite Subset-Family of X st Y is
in_general_position holds Components(Y) is a_partition of X
proof
let X be non empty set;
let Y be finite Subset-Family of X;
assume Y is in_general_position;
then
A1: for A be Subset of X st A in Components(Y) holds A <> {} & for B be
Subset of X st B in Components(Y) holds A = B or A misses B by Th16;
union Components(Y) = X by Th15;
hence thesis by A1,EQREL_1:def 4;
end;
begin :: About basis of Topological Spaces
theorem Th20:
for L be non empty RelStr holds [#]L is infs-closed sups-closed
proof
let L be non empty RelStr;
for X be Subset of [#]L st ex_inf_of X,L holds "/\"(X,L) in [#]L;
hence [#]L is infs-closed by WAYBEL23:19;
for X be Subset of [#]L st ex_sup_of X,L holds "\/"(X,L) in [#]L;
hence thesis by WAYBEL23:20;
end;
theorem Th21:
for L be non empty RelStr holds [#]L is with_bottom with_top
proof
let L be non empty RelStr;
Bottom L in [#]L;
hence [#]L is with_bottom by WAYBEL23:def 8;
Top L in [#]L;
hence thesis by WAYBEL23:def 9;
end;
registration
let L be non empty RelStr;
cluster [#]L -> infs-closed sups-closed with_bottom with_top;
coherence by Th20,Th21;
end;
theorem
for L be continuous sup-Semilattice holds [#]L is CLbasis of L
proof
let L be continuous sup-Semilattice;
now
let x be Element of L;
waybelow x /\ [#]L = waybelow x by XBOOLE_1:28;
hence x = sup (waybelow x /\ [#]L) by WAYBEL_3:def 5;
end;
hence thesis by WAYBEL23:def 7;
end;
theorem
for L be up-complete non empty Poset st L is finite holds the
carrier of L = the carrier of CompactSublatt L
proof
let L be up-complete non empty Poset;
assume
A1: L is finite;
A2: the carrier of L c= the carrier of CompactSublatt L
proof
let z be object;
assume z in the carrier of L;
then reconsider z1 = z as Element of L;
z1 is compact by A1,WAYBEL_3:17;
hence thesis by WAYBEL_8:def 1;
end;
the carrier of CompactSublatt L c= the carrier of L by YELLOW_0:def 13;
hence thesis by A2;
end;
theorem
for L be lower-bounded sup-Semilattice for B be Subset of L st B is
infinite holds card B = card finsups B
proof
let L be lower-bounded sup-Semilattice;
let B be Subset of L;
defpred P[Function, set] means $2 = "\/"(rng $1,L);
assume
A1: B is infinite;
then reconsider B1 = B as non empty Subset of L;
A2: for p be Element of B1* ex u be Element of finsups B1 st P[p, u]
proof
let p be Element of B1*;
A3: rng p c= the carrier of L by XBOOLE_1:1;
now
per cases;
suppose
rng p is empty;
hence ex_sup_of rng p,L by YELLOW_0:42;
end;
suppose
rng p is non empty;
hence ex_sup_of rng p,L by A3,YELLOW_0:54;
end;
end;
then "\/"(rng p,L) in { "\/"(Y,L) where Y is finite Subset of B1 :
ex_sup_of Y,L};
then reconsider u = "\/"(rng p,L) as Element of finsups B1 by
WAYBEL_0:def 27;
take u;
thus thesis;
end;
consider f be Function of B1*,finsups B1 such that
A4: for p be Element of B1* holds P[p, f.p] from FUNCT_2:sch 3(A2);
B c= finsups B
proof
let z be object;
assume
A5: z in B;
then reconsider z1 = z as Element of L;
A6: {z1} c= B
by A5,TARSKI:def 1;
ex_sup_of {z1},L & z = sup {z1} by YELLOW_0:38,39;
then z1 in { "\/"(Y,L) where Y is finite Subset of B : ex_sup_of Y,L } by
A6;
hence thesis by WAYBEL_0:def 27;
end;
then
A7: card B c= card finsups B by CARD_1:11;
A8: dom f = B1* by FUNCT_2:def 1;
finsups B c= rng f
proof
let z be object;
assume z in finsups B;
then z in { "\/"(Y,L) where Y is finite Subset of B : ex_sup_of Y,L } by
WAYBEL_0:def 27;
then consider Y be finite Subset of B such that
A9: z = "\/"(Y,L) and
ex_sup_of Y,L;
consider p be FinSequence such that
A10: rng p = Y by FINSEQ_1:52;
reconsider p as FinSequence of B1 by A10,FINSEQ_1:def 4;
reconsider p1 = p as Element of B1* by FINSEQ_1:def 11;
f.p1 = "\/"(rng p1,L) by A4;
hence thesis by A8,A9,A10,FUNCT_1:def 3;
end;
then card finsups B1 c= card (B1*) by A8,CARD_1:12;
then card finsups B1 c= card B1 by A1,CARD_4:24;
hence thesis by A7;
end;
theorem
for T be T_0 non empty TopSpace holds card the carrier of T c= card
the topology of T
proof
let T be T_0 non empty TopSpace;
defpred P[Element of T, set] means $2 = [#]T \ Cl {$1};
A1: for e be Element of T ex u be Element of the topology of T st P[e, u]
proof
let e be Element of T;
reconsider u = [#]T \ Cl {e} as Element of the topology of T
by PRE_TOPC:def 2,def 3;
take u;
thus thesis;
end;
consider f be Function of the carrier of T, the topology of T such that
A2: for e be Element of T holds P[e, f.e] from FUNCT_2:sch 3(A1);
A3: f is one-to-one
proof
let x1,x2 be object;
assume that
A4: x1 in dom f & x2 in dom f and
A5: f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of T by A4;
(Cl {y1})` = [#]T \ Cl {y1} by SUBSET_1:def 4
.= f.x2 by A2,A5
.= [#]T \ Cl {y2} by A2
.= (Cl {y2})` by SUBSET_1:def 4;
then Cl {y2} c= Cl {y1} & Cl {y1} c= Cl {y2} by SUBSET_1:12;
hence thesis by XBOOLE_0:def 10,YELLOW_8:23;
end;
dom f = the carrier of T & rng f c= the topology of T by FUNCT_2:def 1;
hence thesis by A3,CARD_1:10;
end;
theorem Th26:
for T be TopStruct for X be Subset of T st X is open for B be
finite Subset-Family of T st B is Basis of T for Y be set st Y in Components(B)
holds X misses Y or Y c= X
proof
let T be TopStruct;
let X be Subset of T;
assume X is open;
then
A1: X in the topology of T by PRE_TOPC:def 2;
let B be finite Subset-Family of T;
assume B is Basis of T;
then the topology of T c= UniCl B by CANTOR_1:def 2;
then consider Z be Subset-Family of T such that
A2: Z c= B and
A3: X = union Z by A1,CANTOR_1:def 1;
let Y be set;
consider p be FinSequence of bool the carrier of T such that
len p = card B and
A4: rng p = B and
A5: Components(B) = { Intersect (rng MergeSequence(p,q)) where q is
FinSequence of BOOLEAN : len q = len p } by Def2;
assume Y in Components(B);
then consider q be FinSequence of BOOLEAN such that
A6: Y = Intersect (rng MergeSequence(p,q)) and
len q = len p by A5;
assume X /\ Y <> {};
then consider x be object such that
A7: x in X /\ Y by XBOOLE_0:def 1;
x in X by A7,XBOOLE_0:def 4;
then consider b be set such that
A8: x in b and
A9: b in Z by A3,TARSKI:def 4;
A10: x in Y by A7,XBOOLE_0:def 4;
A11: Y c= b
proof
let z be object;
consider i be Nat such that
A12: i in dom p and
A13: p.i = b by A4,A2,A9,FINSEQ_2:10;
A14: i in dom MergeSequence(p,q) by A12,Th1;
now
per cases by XBOOLEAN:def 3;
suppose
q.i = TRUE;
hence MergeSequence(p,q).i = b by A13,Th2;
end;
suppose
q.i = FALSE;
then
A15: MergeSequence(p,q).i = (the carrier of T) \ b by A12,A13,Th3;
MergeSequence(p,q).i in rng MergeSequence(p,q) by A14,FUNCT_1:def 3;
then Y c= (the carrier of T) \ b by A6,A15,MSSUBFAM:2;
hence MergeSequence(p,q).i = b by A10,A8,XBOOLE_0:def 5;
end;
end;
then
A16: b in rng MergeSequence(p,q) by A14,FUNCT_1:def 3;
assume z in Y;
hence thesis by A6,A16,SETFAM_1:43;
end;
b c= X by A3,A9,ZFMISC_1:74;
hence thesis by A11;
end;
theorem
for T be T_0 TopSpace st T is infinite for B be Basis of T holds B is
infinite
proof
let T be T_0 TopSpace;
assume
A1: T is infinite;
let B be Basis of T;
assume B is finite;
then reconsider B1 = B as finite Subset-Family of T;
union Components(B1) = the carrier of T by Th15;
then consider X be set such that
A2: X in Components(B1) and
A3: X is infinite by A1,FINSET_1:7;
reconsider X as infinite set by A3;
consider x be object such that
A4: x in X by XBOOLE_0:def 1;
consider y be object such that
A5: y in X and
A6: x <> y by A4,SUBSET_1:48;
reconsider x1 = x, y1 = y as Element of T by A2,A4,A5;
consider Y be Subset of T such that
A7: Y is open and
A8: x1 in Y & not y1 in Y or y1 in Y & not x1 in Y by A1,A6,T_0TOPSP:def 7;
now
per cases by A8;
suppose
A9: x in Y & not y in Y;
then x in Y /\ X by A4,XBOOLE_0:def 4;
then X c= Y by A2,A7,Th26,XBOOLE_0:4;
hence contradiction by A5,A9;
end;
suppose
A10: y in Y & not x in Y;
then y in Y /\ X by A5,XBOOLE_0:def 4;
then X c= Y by A2,A7,Th26,XBOOLE_0:4;
hence contradiction by A4,A10;
end;
end;
hence contradiction;
end;
theorem
for T be non empty TopSpace st T is finite for B be Basis of T for x
be Element of T holds meet { A where A is Element of the topology of T : x in A
} in B
proof
deffunc F(set) = $1;
let T be non empty TopSpace;
assume T is finite;
then reconsider tT = the topology of T as finite non empty set;
let B be Basis of T;
let x be Element of T;
defpred P[set] means x in $1;
{ A where A is Element of the topology of T : x in A } c= bool the
carrier of T
proof
let z be object;
assume z in { A where A is Element of the topology of T : x in A };
then ex A be Element of the topology of T st z = A & x in A;
hence thesis;
end;
then reconsider
sfA = { A where A is Element of the topology of T : x in A } as
Subset-Family of T;
reconsider sfA as Subset-Family of T;
A1: now
let Y be set;
assume Y in sfA;
then ex A be Element of the topology of T st Y = A & x in A;
hence x in Y;
end;
the carrier of T is Element of the topology of T by PRE_TOPC:def 1;
then the carrier of T in sfA;
then
A2: x in meet sfA by A1,SETFAM_1:def 1;
A3: now
let P be Subset of T;
assume P in sfA;
then ex A be Element of the topology of T st P = A & x in A;
hence P is open by PRE_TOPC:def 2;
end;
{ F(A) where A is Element of tT : P[A] } is finite from PRE_CIRC:sch 1;
then meet sfA is open by A3,TOPS_2:20,def 1;
then consider a be Subset of T such that
A4: a in B and
A5: x in a and
A6: a c= meet sfA by A2,YELLOW_9:31;
meet sfA c= a
proof
let z be object;
B c= the topology of T by TOPS_2:64;
then a in sfA by A4,A5;
hence thesis by SETFAM_1:def 1;
end;
hence thesis by A4,A6,XBOOLE_0:def 10;
end;