:: Finite Product of Semiring of Sets
:: by Roland Coghetto
::
:: Received April 19, 2015
:: Copyright (c) 2015-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 ARYTM_3, CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FINSUB_1, FUNCT_1,
RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI, XBOOLE_0,
ZFMISC_1, CARD_1, TEX_1, PRE_TOPC, RCOMP_1, STRUCT_0, FUNCT_2, SRINGS_4,
NAT_1, XCMPLX_0, FINSEQ_2, ORDINAL4, XXREAL_0, SRINGS_3;
notations TARSKI, XBOOLE_0, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1, CARD_3,
ZFMISC_1, FINSUB_1, FUNCT_1, SIMPLEX0, CARD_1, STRUCT_0, PRE_TOPC,
BINOP_1, TEX_1, ENUMSET1, ORDINAL1, RELAT_1, RELSET_1, FUNCT_2, XCMPLX_0,
XXREAL_0, SRINGS_1, FINSEQ_1, FINSEQ_2, SRINGS_3;
constructors COHSP_1, SRINGS_1, TEX_1, TOPREALB, SRINGS_3;
registrations FINSET_1, RELAT_1, RELSET_1, SIMPLEX0, SUBSET_1, COHSP_1,
ORDINAL1, ZFMISC_1, STRUCT_0, SRINGS_1, CARD_3, EQREL_1, FINSEQ_1,
FUNCT_1, NAT_1, CARD_1, PRE_TOPC, FUNCT_2, XCMPLX_0, XXREAL_0, FINSEQ_2,
SRINGS_3, SRINGS_2, XBOOLE_0, AOFA_000;
requirements BOOLE, NUMERALS, SUBSET;
definitions TARSKI, XBOOLE_0, EQREL_1, FINSUB_1, SRINGS_1;
equalities CARD_3, TEX_1;
expansions FINSUB_1, XBOOLE_0, TARSKI, SRINGS_1, SETFAM_1;
theorems EQREL_1, FINSEQ_1, FINSUB_1, FUNCT_2, SETFAM_1, TARSKI, XBOOLE_0,
XBOOLE_1, ZFMISC_1, PRE_TOPC, STRUCT_0, PRVECT_3, ENUMSET1, CARD_3,
FUNCT_1, RELAT_1, SUBSET_1, PARTFUN1, CARD_1, SRINGS_1, SRINGS_2,
FUNCT_5, FUNCT_6, NAT_1, FINSET_1, XCMPLX_1, FINSEQ_3, FINSEQ_2, BINOP_1,
FINSEQ_5, SRINGS_3, WAYBEL12;
schemes FUNCT_1, FRAENKEL, FINSEQ_1, NAT_1, XBOOLE_0;
begin :: Preliminaries
reserve X1,X2,X3,X4 for set;
Thm01:
((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ (X2 \/ X3 \/ X4)) is empty &
((X1 /\ X4) \ (X2 \/ X3)) /\ ((X1 /\ X3 /\ X4) \ X2) is empty &
(X1 \ (X2 \/ X3 \/ X4)) /\ ((X1 /\ X3 /\ X4) \ X2) is empty
proof
thus ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ (X2 \/ X3 \/ X4)) is empty
proof
let t be object;
assume t in ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ (X2 \/ X3 \/ X4));
then t in ((X1 /\ X4) \ (X2 \/ X3)) & t in (X1 \ (X2 \/ X3 \/ X4))
by XBOOLE_0:def 4;
then t in (X1/\X4) & not t in (X2\/X3) & t in X1 & not t in X2\/X3\/X4
by XBOOLE_0:def 5;
then (t in X1 & t in X4) & not (t in X2 & t in X3) & t in X1 &
not ((t in X2 or t in X3) or t in X4)
by XBOOLE_0:def 3,XBOOLE_0:def 4;
hence contradiction;
end;
thus ((X1 /\ X4) \ (X2 \/ X3)) /\ ((X1 /\ X3 /\ X4) \ X2) is empty
proof
let t be object;
assume t in ((X1 /\ X4) \ (X2 \/ X3)) /\ ((X1 /\ X3 /\ X4) \ X2);
then t in (X1 /\ X4) \ (X2 \/ X3) & t in (X1 /\ X3 /\ X4) \ X2
by XBOOLE_0:def 4;
then t in X1 /\ X4 & not t in X2 \/ X3 & t in (X1 /\ X3 /\ X4) &
not t in X2 by XBOOLE_0:def 5;
then t in X1 & t in X4 & not (t in X2 or t in X3) & t in (X1 /\ X3) &
t in X4 & not t in X2 by XBOOLE_0:def 3,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 4;
end;
let t be object;
assume t in (X1 \ (X2 \/ X3 \/ X4)) /\ ((X1 /\ X3 /\ X4) \ X2);
then t in X1 \ (X2 \/ X3 \/ X4) & t in (X1 /\ X3 /\ X4) \ X2
by XBOOLE_0:def 4;
then t in X1 & not t in X2 \/ X3 \/ X4 & t in X1 /\ X3 /\ X4 &
not t in X2 by XBOOLE_0:def 5;
then t in X1 & not t in (X2 \/ X3) & not t in X4 & t in X1 /\ X3 &
t in X4 & not t in X2 by XBOOLE_0:def 3,XBOOLE_0:def 4;
hence contradiction;
end;
theorem
((X1 /\ X4) \ (X2 \/ X3)) misses (X1 \ (X2 \/ X3 \/ X4)) &
((X1 /\ X4) \ (X2 \/ X3)) misses ((X1 /\ X3 /\ X4) \ X2) &
(X1 \ (X2 \/ X3 \/ X4)) misses ((X1 /\ X3 /\ X4) \ X2) by Thm01;
theorem Thm02:
(X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)
proof
hereby
let t be object;
assume t in (X1 \ X2) \ (X3 \ X4);
then t in X1 \ X2 & not t in X3 \ X4 by XBOOLE_0:def 5;
then t in X1 & not t in X2 & (not t in X3 or t in X4) by XBOOLE_0:def 5;
then (t in X1 & not (t in X2 or t in X3)) or
t in X1/\X4 & not t in X2 by XBOOLE_0:def 4;
then (t in X1 & not t in X2\/X3) or
t in ((X1/\X4)\X2) by XBOOLE_0:def 3,def 5;
then t in X1 \ (X2 \/ X3) or t in ((X1 /\ X4) \ X2) by XBOOLE_0:def 5;
hence t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) by XBOOLE_0:def 3;
end;
let t be object;
assume t in (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2);
then t in X1 \ (X2 \/ X3) or t in (X1 /\ X4) \ X2 by XBOOLE_0:def 3;
then (t in X1 & not t in X2 \/ X3) or
(t in (X1 /\ X4) & not t in X2) by XBOOLE_0:def 5;
then (t in X1 & not t in X2 & not t in X3) or
(t in X1 & t in X4 & not t in X2) by XBOOLE_0:def 3,def 4;
then t in X1\X2 & not t in X3\X4 by XBOOLE_0:def 5;
hence t in (X1 \ X2) \ (X3 \ X4) by XBOOLE_0:def 5;
end;
Lm1:
X1 \ (X2 \/ X3) c=
((X1 /\ X4) \ (X2 \/ X3)) \/
(X1 \ (X2 \/ X3 \/ X4)) \/ ((X1 /\ X3 /\ X4) \ X2)
proof
let t be object;
assume t in X1\(X2\/X3);
then t in X1 & not t in X2\/X3 by XBOOLE_0:def 5;
then (t in X1 & t in X4 & not (t in X2 or t in X3)) or
(t in X1 & not (t in X2\/X3 or t in X4)) or
(t in X1/\X3 & t in X4 & not t in X2) by XBOOLE_0:def 3;
then (t in X1/\X4 & not (t in X2\/X3)) or
(t in X1 & not (t in (X2 \/ X3 \/ X4))) or
(t in (X1 /\ X3 /\ X4) & not t in X2) by XBOOLE_0:def 3,def 4;
then t in (X1/\X4)\(X2\/X3) or t in (X1 \ (X2 \/ X3 \/ X4)) or
t in ((X1 /\ X3 /\ X4) \ X2) by XBOOLE_0:def 5;
then t in (X1/\X4)\(X2\/X3)\/(X1 \ (X2 \/ X3 \/ X4)) or
t in ((X1 /\ X3 /\ X4) \ X2) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
Lm2:
(X1 /\ X4) \ X2 c= ((X1 /\ X4) \ (X2 \/ X3)) \/
(X1 \ (X2 \/ X3 \/ X4)) \/ ((X1 /\ X3 /\ X4) \ X2)
proof
let t be object;
assume t in (X1 /\ X4) \ X2;
then (t in X1 & t in X4 & not t in X2 & not t in X3) or
(t in X1 & (not t in X2 & not t in X3 & not t in X4)) or
(t in X1 & t in X3 & t in X4 & not t in X2)
by XBOOLE_0:def 4,XBOOLE_0:def 5;
then (t in X1 & t in X4 & not (t in X2 or t in X3)) or
(t in X1 & not (t in X2\/X3 or t in X4)) or
(t in X1/\X3 & t in X4 & not t in X2) by XBOOLE_0:def 3,def 4;
then (t in X1/\X4 & not (t in X2\/X3)) or
(t in X1 & not (t in (X2 \/ X3 \/ X4))) or
(t in (X1 /\ X3 /\ X4) & not t in X2) by XBOOLE_0:def 3,def 4;
then t in (X1/\X4)\(X2\/X3) or t in (X1 \ (X2 \/ X3 \/ X4)) or
t in ((X1 /\ X3 /\ X4) \ X2) by XBOOLE_0:def 5;
then t in (X1/\X4)\(X2\/X3)\/(X1 \ (X2 \/ X3 \/ X4)) or
t in ((X1 /\ X3 /\ X4) \ X2) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
Lm3:
(X1 /\ X3 /\ X4) \ X2 c= (X1 /\ X4) \ X2
proof
X1 /\ X3 /\ X4 = X1 /\ X4 /\ X3 by XBOOLE_1:16;
hence thesis by XBOOLE_1:17,XBOOLE_1:33;
end;
theorem Thm03:
(X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) =
((X1 /\ X4) \ (X2 \/ X3)) \/
(X1 \ (X2 \/ X3 \/ X4)) \/ ((X1 /\ X3 /\ X4) \ X2)
proof
set M1=X1 \ (X2 \/ X3);
set M2=(X1 /\ X4) \ X2;
set M3=((X1 /\ X4) \ (X2 \/ X3));
set M4=(X1 \ (X2 \/ X3 \/ X4));
set M5=((X1 /\ X3 /\ X4) \ X2);
set Z=M3 \/ M4 \/ M5;
M1 c= Z & M2 c= Z by Lm1,Lm2;
then M1 \/ M2 c= Z \/ Z by XBOOLE_1:13;
hence M1 \/ M2 c= Z;
M3 c= M2 & M4 c= M1 & M5 c= M2 by XBOOLE_1:7,XBOOLE_1:34,Lm3;
then M3 \/ M4 c= (M1 \/ M2) \/ (M1 \/ M2) & M5 c= M1 \/ M2
by XBOOLE_1:10,XBOOLE_1:13;
hence M3 \/ M4 \/ M5 c= M1 \/ M2 by XBOOLE_1:13;
end;
theorem Thm04:
(X1 \ X2) \ (X3 \ X4) = ((X1 /\ X4) \ (X2 \/ X3)) \/
(X1 \ (X2 \/ X3 \/ X4)) \/ ((X1 /\ X3 /\ X4) \ X2)
proof
(X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) by Thm02;
hence thesis by Thm03;
end;
theorem Thm05:
union {X1,X2,X3} = X1 \/ X2 \/ X3
proof
thus union {X1,X2,X3} = union ({X1,X2} \/ {X3}) by ENUMSET1:3
.= union {X1,X2} \/ union {X3} by ZFMISC_1:78
.= X1 \/ X2 \/ union {X3} by ZFMISC_1:75
.= X1 \/ X2 \/ X3;
end;
begin :: Image of a Semiring of Sets by an Injective Function
theorem Thm07:
for T,S being set, f being Function of T,S,
G being Subset-Family of T holds
f.:G = {f.:A where A is Subset of T : A in G}
proof
let T,S be set,
f be Function of T,S,
G be Subset-Family of T;
hereby
let t be object;
assume
A1: t in f.:G;
then reconsider t1=t as Subset of S;
consider B be Subset of T such that
A2: B in G and
A3: t1 = f.:B by A1,FUNCT_2:def 10;
thus t in {f.:A where A is Subset of T:A in G} by A2,A3;
end;
let t be object;
assume t in {f.:A where A is Subset of T:A in G};
then consider A be Subset of T such that
A4: t = f.:A and
A5: A in G;
thus t in f.:G by A4,A5,FUNCT_2:def 10;
end;
registration
let T,S be set,
f be Function of T,S,
G be finite Subset-Family of T;
cluster f.:G -> finite;
coherence
proof
A1: G is finite;
deffunc F(Element of bool T) = f.:$1;
{F(A) where A is Element of bool T:A in G} is finite
from FRAENKEL:sch 21(A1);
hence thesis by Thm07;
end;
end;
registration
let f be Function, A be countable set;
cluster f.:A -> countable;
coherence
proof
card (f.:A) c= card A by CARD_1:67;
hence thesis by WAYBEL12:1;
end;
end;
scheme
FraenkelCountable { A() -> set, X() -> set, F(object) -> set }:
{ F(w) where w is Element of A(): w in X() } is countable
provided
A1: X() is countable
proof
set M = { F(w) where w is Element of A(): w in X() };
per cases;
suppose
A2: A() is empty;
M c= {F({})}
proof
let x be object;
assume x in M;
then consider w being Element of A() such that
A3: x = F(w) & w in X();
w = {} by A2,SUBSET_1:def 1;
hence thesis by A3,TARSKI:def 1;
end;
hence thesis;
end;
suppose
A4: A() is non empty;
consider f being Function such that
A5: dom f = X() /\ A() and
A6: for y being object st y in X() /\ A() holds f.y = F(y)
from FUNCT_1:sch 3;
M = f.:X()
proof
thus M c= f.:X()
proof
let x be object;
assume x in M;
then consider u being Element of A() such that
A7: x = F(u) and
A8: u in X();
A9: u in dom f by A4,A5,A8,XBOOLE_0:def 4;
then f.u = F(u) by A5,A6;
hence thesis by A7,A8,A9,FUNCT_1:def 6;
end;
let x be object;
assume x in f.:X();
then consider y being object such that
A10: y in dom f and
A11: y in X() and
A12: x = f.y by FUNCT_1:def 6;
reconsider y as Element of A() by A5,A10,XBOOLE_0:def 4;
x = F(y) by A5,A6,A10,A12;
hence thesis by A11;
end;
hence thesis by A1;
end;
end;
registration
let T,S be set,
f be Function of T,S,
G be countable Subset-Family of T;
cluster f.:G -> countable;
coherence
proof
A1: G is countable;
deffunc F(Element of bool T) = f.:$1;
{F(A) where A is Element of bool T:A in G} is countable
from FraenkelCountable(A1);
hence thesis by Thm07;
end;
end;
Thm08:
for X,Y being set,S being with_empty_element Subset-Family of X,
f being Function of X,Y
holds f.:S is with_empty_element Subset-Family of Y
proof
let X,Y be set,S be with_empty_element Subset-Family of X,
f be Function of X,Y;
{} is Subset of Y & {} is Subset of X & {} in S & {}=f.:{}
by SETFAM_1:def 8;
then {} in f.:S by FUNCT_2:def 10;
hence thesis;
end;
registration
let X,Y be set,S be with_empty_element Subset-Family of X,
f be Function of X,Y;
cluster f.:S -> with_empty_element;
coherence by Thm08;
end;
theorem
for X,Y being set,f being Function of X,Y,
SF1,SF2 being Subset-Family of X st SF1 c= SF2
holds f.:SF1 c= f.:SF2
proof
let X,Y be set,f be Function of X,Y,
SF1,SF2 be Subset-Family of X;
assume
A1: SF1 c= SF2;
A2: f.:SF1 = {f.:A where A is Subset of X:A in SF1} &
f.:SF2 = {f.:A where A is Subset of X: A in SF2} by Thm07;
let x be object;
assume x in f.:SF1;
then consider A be Subset of X such that
A3: x=f.:A and
A4: A in SF1 by A2;
thus x in f.:SF2 by A1,A2,A3,A4;
end;
theorem Thm10:
for X,Y being set,S being cap-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one
holds f.:S is cap-closed Subset-Family of Y
proof
let X,Y be set,
S be cap-closed Subset-Family of X,
f be Function of X,Y;
assume
A1: f is one-to-one;
now
let s1,s2 be set;
assume
A2: s1 in f.:S & s2 in f.:S;
consider c1 be Subset of X such that
A3: c1 in S and
A4: s1=f.:c1 by A2,FUNCT_2:def 10;
consider c2 be Subset of X such that
A5: c2 in S and
A6: s2=f.:c2 by A2,FUNCT_2:def 10;
reconsider f12=f.:(c1/\c2) as Subset of Y;
c1/\c2 in S by A3,A5,FINSUB_1:def 2;
then f12 in f.:S by FUNCT_2:def 10;
hence s1/\s2 in f.:S by A1,A4,A6,FUNCT_1:62;
end;
hence thesis by FINSUB_1:def 2;
end;
theorem Thm11:
for X,Y being non empty set,
S being cap-finite-partition-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one
holds f.:S is cap-finite-partition-closed Subset-Family of Y
proof
let X,Y be non empty set,
S be cap-finite-partition-closed Subset-Family of X,
f be Function of X,Y;
assume
A1: f is one-to-one;
per cases;
suppose f.:S is empty;
hence thesis;
end;
suppose
A2: f.:S is non empty;
reconsider fS=f.:S as Subset-Family of Y;
fS is cap-finite-partition-closed
proof
let s1,s2 be Element of fS;
assume
A3: s1/\s2 is non empty;
A4: s1 in fS by A2;
consider c1 be Subset of X such that
A5: c1 in S and
A6: s1=f.:c1 by A4,FUNCT_2:def 10;
A7: s2 in fS by A2;
consider c2 be Subset of X such that
A8: c2 in S and
A9: s2=f.:c2 by A7,FUNCT_2:def 10;
A10: f.:(c1/\c2) = s1/\s2 by A1,A6,A9,FUNCT_1:62;
then
A11: c1/\c2 is non empty by A3;
consider x1 be finite Subset of S such that
A12: x1 is a_partition of c1/\c2 by A5,A8,A11,SRINGS_1:def 1;
x1 c= S & S c= bool X;
then x1 c= bool X;
then reconsider x2=x1 as Subset-Family of X;
now
thus f.:x2 is finite Subset of fS by FUNCT_2:103;
thus f.:x2 is a_partition of s1/\s2
proof
now
f.:x2 c= bool (s1/\s2)
proof
let t be object;
assume t in f.:x2;
then consider y1 be Subset of X such that
A13: y1 in x2 and
A14: t = f.:y1 by FUNCT_2:def 10;
reconsider t1=t as set by A14;
f.:y1 c= f.:(c1/\c2) by A12,A13,RELAT_1:123;
then t1 c= (s1/\s2) by A14,A1,A6,A9,FUNCT_1:62;
hence t in bool (s1/\s2);
end;
hence f.:x2 is Subset-Family of s1/\s2;
now
hereby
let t be object;
assume t in union (f.:x2);
then consider u be set such that
A15: t in u and
A16: u in f.:x2 by TARSKI:def 4;
consider v be Subset of X such that
A17: v in x2 and
A18: u = f.:v by A16,FUNCT_2:def 10;
f.:v c= f.:(c1/\c2) by A12,A17,RELAT_1:123;
hence t in s1/\s2 by A15,A18,A10;
end;
let t be object;
assume t in s1/\s2;
then t in f.:(c1/\c2) by A1,A6,A9,FUNCT_1:62;
then consider v be object such that
A19: v in dom f and
A20: v in c1/\c2 and
A21: t=f.v by FUNCT_1:def 6;
v in union x1 by A12,A20,EQREL_1:def 4;
then consider u be set such that
A22: v in u and
A23: u in x1 by TARSKI:def 4;
reconsider fu=f.:u as Subset of Y;
f.v in f.:u & f.:u in f.:x2
by A19,A22,FUNCT_1:def 6,A23,FUNCT_2:def 10;
hence t in union (f.:x2) by A21,TARSKI:def 4;
end;
hence union (f.:x2) = s1/\s2 by TARSKI:def 3;
now
let A be Subset of s1/\s2;
assume A in f.:x2;
then consider a0 be Subset of X such that
A26: a0 in x2 and
A27: A = f.:a0 by FUNCT_2:def 10;
thus A <> {}
proof
assume
A28: A = {};
dom f = X by PARTFUN1:def 2;
hence contradiction by A26,A12,A28,A27;
end;
let B be Subset of s1/\s2;
assume B in f.:x2;
then consider b0 be Subset of X such that
A29: b0 in x2 and
A30: B = f.:b0 by FUNCT_2:def 10;
thus A=B or A misses B
by A26,A29,A12,EQREL_1:def 4,A27,A30,A1,FUNCT_1:66;
end;
hence for A be Subset of s1/\s2 st A in f.:x2 holds
A <> {} &
for B be Subset of s1/\s2 st B in f.:x2 holds
A=B or A misses B;
end;
hence thesis by EQREL_1:def 4;
end;
end;
hence ex x be finite Subset of fS st x is a_partition of s1/\s2;
end;
hence thesis;
end;
end;
theorem Thm12:
for X,Y being non empty set,
S being diff-c=-finite-partition-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one & f.:S is non empty
holds f.:S is diff-c=-finite-partition-closed Subset-Family of Y
proof
let X,Y be non empty set,
S be diff-c=-finite-partition-closed Subset-Family of X,
f be Function of X,Y;
assume that
A1: f is one-to-one and
A2: f.:S is non empty;
reconsider fS=f.:S as Subset-Family of Y;
fS is diff-c=-finite-partition-closed
proof
let s1,s2 be Element of fS;
assume
A3: s2 c= s1;
s1 in fS by A2;
then consider c1 be Subset of X such that
A4: c1 in S and
A5: s1=f.:c1 by FUNCT_2:def 10;
s2 in fS by A2;
then consider c2 be Subset of X such that
A6: c2 in S and
A7: s2=f.:c2 by FUNCT_2:def 10;
A8: f.:(c1\c2)=s1\s2 by A1,A5,A7,FUNCT_1:64;
dom f = X by PARTFUN1:def 2;
then consider y1 be finite Subset of S such that
A9: y1 is a_partition of c1\c2
by A3,A5,A7,A1,FUNCT_1:87,A4,A6,SRINGS_1:def 3;
y1 c= S & S c= bool X;
then y1 c= bool X;
then reconsider y2=y1 as Subset-Family of X;
thus ex x be finite Subset of fS st x is a_partition of s1\s2
proof
reconsider fy = f.:y2 as finite Subset of fS by FUNCT_2:103;
take fy;
now
f.:y2 c= bool (s1\s2)
proof
let t be object;
assume t in f.:y2;
then consider z1 be Subset of X such that
A10: z1 in y2 and
A11: t = f.:z1 by FUNCT_2:def 10;
reconsider t1=t as set by A11;
f.:z1 c= f.:(c1\c2) by A9,A10,RELAT_1:123;
hence t in bool (s1\s2) by A11,A8;
end;
hence f.:y2 is Subset-Family of s1\s2;
now
hereby
let t be object;
assume t in union (f.:y2);
then consider u be set such that
A12: t in u and
A13: u in f.:y2 by TARSKI:def 4;
consider v be Subset of X such that
A14: v in y2 and
A15: u=f.:v by A13,FUNCT_2:def 10;
f.:v c= f.:(c1\c2) by A14,A9,RELAT_1:123;
hence t in s1\s2 by A12,A15,A8;
end;
let t be object;
assume t in s1\s2;
then t in f.:(c1\c2) by A1,A5,A7,FUNCT_1:64;
then consider v be object such that
A16: v in dom f and
A17: v in c1\c2 and
A18: t=f.v by FUNCT_1:def 6;
v in union y1 by A9,A17,EQREL_1:def 4;
then consider u be set such that
A19: v in u and
A20: u in y1 by TARSKI:def 4;
reconsider fu=f.:u as Subset of Y;
f.v in f.:u & f.:u in f.:y2 by A16,A19,FUNCT_1:def 6,
A20,FUNCT_2:def 10;
hence t in union (f.:y2) by A18,TARSKI:def 4;
end;
hence union (f.:y2)=s1\s2 by TARSKI:def 3;
thus for A be Subset of s1\s2 st A in f.:y2 holds
A<>{} & for B be Subset of s1\s2 st B in f.:y2 holds
A=B or A misses B
proof
let A be Subset of s1\s2;
assume A in f.:y2;
then consider a0 be Subset of X such that
A23: a0 in y2 and
A24: A = f.:a0 by FUNCT_2:def 10;
thus A <> {}
proof
assume
A25: A={};
dom f = X by PARTFUN1:def 2;
hence contradiction by A23,A9,A25,A24;
end;
let B be Subset of s1\s2;
assume B in f.:y2;
then consider b0 be Subset of X such that
A26: b0 in y2 and
A27: B = f.:b0 by FUNCT_2:def 10;
thus thesis by A23,A24,A26,A27,A1,A9,EQREL_1:def 4,FUNCT_1:66;
end;
end;
hence thesis by EQREL_1:def 4;
end;
end;
hence thesis;
end;
theorem
for X,Y being non empty set,
S being diff-finite-partition-closed Subset-Family of X,
f being Function of X,Y st f is one-to-one
holds f.:S is diff-finite-partition-closed Subset-Family of Y
proof
let X,Y be non empty set,
S be diff-finite-partition-closed Subset-Family of X,
f be Function of X,Y;
assume
A1: f is one-to-one;
per cases;
suppose f.:S is empty;
then for S1,S2 be Element of f.:S st S1\S2 is non empty holds
f.:S is diff-finite-partition-closed by SUBSET_1:def 1;
then f.:S is diff-finite-partition-closed;
hence thesis;
end;
suppose
A2: f.:S is non empty;
reconsider fS=f.:S as Subset-Family of Y;
now
let s1,s2 be Element of fS;
assume
A3: s1\s2 is non empty;
A4: s1 in fS by A2;
consider c1 be Subset of X such that
A5: c1 in S and
A6: s1=f.:c1 by A4,FUNCT_2:def 10;
A7: s2 in fS by A2;
consider c2 be Subset of X such that
A8: c2 in S and
A9: s2=f.:c2 by A7,FUNCT_2:def 10;
A10: f.:(c1\c2) = s1\s2 by A1,A6,A9,FUNCT_1:64;
then
A11: c1\c2 is non empty by A3;
consider x1 be finite Subset of S such that
A12: x1 is a_partition of c1\c2 by A5,A8,A11,SRINGS_1:def 2;
x1 c= S & S c= bool X;
then x1 c= bool X;
then reconsider x2=x1 as Subset-Family of X;
now
thus f.:x2 is finite Subset of fS by FUNCT_2:103;
thus f.:x2 is a_partition of s1\s2
proof
now
f.:x2 c= bool (s1\s2)
proof
let t be object;
assume t in f.:x2;
then consider y1 be Subset of X such that
A13: y1 in x2 and
A14: t = f.:y1 by FUNCT_2:def 10;
reconsider t1=t as set by A14;
f.:y1 c= f.:(c1\c2) by A12,A13,RELAT_1:123;
then t1 c= (s1\s2) by A14,A1,A6,A9,FUNCT_1:64;
hence t in bool (s1\s2);
end;
hence f.:x2 is Subset-Family of s1\s2;
now
hereby
let t be object;
assume t in union (f.:x2);
then consider u be set such that
A15: t in u and
A16: u in f.:x2 by TARSKI:def 4;
consider v be Subset of X such that
A17: v in x2 and
A18: u = f.:v by A16,FUNCT_2:def 10;
f.:v c= f.:(c1\c2) by A12,A17,RELAT_1:123;
hence t in s1\s2 by A15,A18,A10;
end;
let t be object;
assume t in s1\s2;
then t in f.:(c1\c2) by A1,A6,A9,FUNCT_1:64;
then consider v be object such that
A19: v in dom f and
A20: v in c1\c2 and
A21: t=f.v by FUNCT_1:def 6;
v in union x1 by A12,A20,EQREL_1:def 4;
then consider u be set such that
A22: v in u and
A23: u in x1 by TARSKI:def 4;
reconsider fu=f.:u as Subset of Y;
f.v in f.:u & f.:u in f.:x2
by A19,A22,FUNCT_1:def 6,A23,FUNCT_2:def 10;
hence t in union (f.:x2) by A21,TARSKI:def 4;
end;
hence union (f.:x2) = s1\s2 by TARSKI:def 3;
now
let A be Subset of s1\s2;
assume A in f.:x2;
then consider a0 be Subset of X such that
A26: a0 in x2 and
A27: A = f.:a0 by FUNCT_2:def 10;
thus A <> {}
proof
assume
A28: A = {};
dom f = X by PARTFUN1:def 2;
hence contradiction by A26,A12,A28,A27;
end;
hereby
let B be Subset of s1\s2;
assume B in f.:x2;
then consider b0 be Subset of X such that
A29: b0 in x2 and
A30: B = f.:b0 by FUNCT_2:def 10;
thus A=B or A misses B
by A26,A29,A12,EQREL_1:def 4,A27,A30,A1,FUNCT_1:66;
end;
end;
hence for A be Subset of s1\s2 st A in f.:x2 holds
A <> {} & for B be Subset of s1\s2 st B in f.:x2 holds
A=B or A misses B;
end;
hence thesis by EQREL_1:def 4;
end;
end;
hence ex x be finite Subset of fS st x is a_partition of s1\s2;
end;
then fS is diff-finite-partition-closed;
hence thesis;
end;
end;
theorem
for X,Y being non empty set,S being semiring_of_sets of X,
f being Function of X,Y st f is one-to-one
holds f.:S is semiring_of_sets of Y by Thm11,Thm12;
begin
::$CT
registration
let X be set;
cluster cobool X -> cap-closed;
coherence
proof
set D = cobool X;
for x,y being set st x in D & y in D holds x /\ y in D
proof
let x,y be set;
assume x in D & y in D; then
per cases by TARSKI:def 2;
suppose x = {};
hence thesis by TARSKI:def 2;
end;
suppose x = X & y = X;
hence thesis by TARSKI:def 2;
end;
suppose x = X & y = {};
hence thesis by TARSKI:def 2;
end;
end;
hence thesis;
end;
end;
registration
let X be set;
cluster with_empty_element for cap-closed Subset-Family of X;
existence
proof
take cobool X;
thus thesis;
end;
end;
registration
let X be set;
cluster cup-closed for with_empty_element cap-closed Subset-Family of X;
existence
proof
cobool X is cup-closed
proof
let a,b be set;
assume a in cobool X & b in cobool X;
then a={} & b={} or a=X & b={} or a={} & b=X or a=X & b=X
by TARSKI:def 2;
hence a\/b in cobool X by TARSKI:def 2;
end;
hence thesis;
end;
end;
registration
let X,Y be non empty set;
cluster DIFFERENCE (X,Y) -> non empty;
correctness
proof
consider x be object such that
A1: x in X by XBOOLE_0:def 1;
reconsider x as Element of X by A1;
consider y be object such that
A2: y in Y by XBOOLE_0:def 1;
reconsider y as Element of Y by A2;
x \ y in DIFFERENCE(X,Y) by SETFAM_1:def 6;
hence DIFFERENCE(X,Y) is non empty;
end;
end;
theorem LemY:
for X be set,
S be with_empty_element Subset-Family of X holds
DIFFERENCE (S,S) = the set of all A \ B where A, B is Element of S
proof
let X be set,
S be with_empty_element Subset-Family of X;
thus DIFFERENCE (S,S) c= the set of all A \ B where A, B is Element of S
proof
let x be object;
assume x in DIFFERENCE (S,S); then
consider X,Y being set such that
A1: X in S & Y in S & x = X \ Y by SETFAM_1:def 6;
thus thesis by A1;
end;
let x be object;
assume x in the set of all A \ B where A, B is Element of S; then
consider A1, B1 being Element of S such that
A2: x = A1 \ B1;
thus thesis by A2,SETFAM_1:def 6;
end;
definition
let X be set,
S be with_empty_element Subset-Family of X;
func semidiff S -> Subset-Family of X equals
DIFFERENCE (S,S);
coherence
proof
set AB = the set of all A \ B where A,B is Element of S;
AB c= bool X
proof
let t be object;
assume t in the set of all A \ B where A,B is Element of S;
then consider A0,B0 be Element of S such that
A1: t = A0 \ B0;
thus t in bool X by A1;
end;
then reconsider AB as Subset-Family of X;
{} in S by SETFAM_1:def 8;
then {} \ {} in AB;
hence thesis by LemY;
end;
end;
theorem LemX1:
for X be set,
S be with_empty_element Subset-Family of X,
x be object st x in semidiff S holds
ex A, B being Element of S st x = A \ B
proof
let X be set,
S be with_empty_element Subset-Family of X,
x be object;
assume x in semidiff S; then
x in the set of all A \ B where A, B is Element of S by LemY;
hence thesis;
end;
registration
let X be set,
S be with_empty_element Subset-Family of X;
cluster semidiff S -> with_empty_element;
coherence
proof
set AB=the set of all A \ B where A,B is Element of S;
AB c= bool X
proof
let t be object;
assume t in the set of all A \ B where A,B is Element of S;
then consider A0,B0 be Element of S such that
A1: t = A0 \ B0;
thus t in bool X by A1;
end;
then reconsider AB as Subset-Family of X;
{} in S by SETFAM_1:def 8;
then {} \ {} in AB;
hence thesis by LemY;
end;
end;
Thm14:
for X being set,
S being with_empty_element cap-closed cup-closed Subset-Family of X holds
semidiff S is cap-closed diff-finite-partition-closed
proof
let X be set,
S be with_empty_element cap-closed cup-closed Subset-Family of X;
thus semidiff S is cap-closed
proof
let s1,s2 be set;
assume
A1: s1 in semidiff S & s2 in semidiff S; then
consider a1,b1 be Element of S such that
A2: s1 = a1 \ b1 by LemX1;
consider a2,b2 be Element of S such that
A3: s2 = a2 \ b2 by A1,LemX1;
A4: s1 /\ s2 = ((a1 \ b1) /\ a2) \ b2 by A2,A3,XBOOLE_1:49
.= ((a1 /\ a2) \ b1) \ b2 by XBOOLE_1:49
.= (a1 /\ a2) \ (b1 \/ b2) by XBOOLE_1:41;
a1 /\ a2 is Element of S &
b1 \/ b2 is Element of S by FINSUB_1:def 1,FINSUB_1:def 2;
hence s1 /\ s2 in semidiff S by A4,SETFAM_1:def 6;
end;
thus semidiff S is diff-finite-partition-closed
proof
let s1,s2 be Element of semidiff S;
assume
A5: s1\s2 is non empty;
consider a1,b1 be Element of S such that
A6: s1 = a1 \ b1 by LemX1;
consider a2,b2 be Element of S such that
A7: s2 = a2 \ b2 by LemX1;
A8: a1/\b2 in S by FINSUB_1:def 2;
a1/\a2 in S by FINSUB_1:def 2; then
A9: a1/\a2/\b2 in S by FINSUB_1:def 2;
A10: b1\/a2 in S by FINSUB_1:def 1; then
A11: b1\/a2\/b2 in S by FINSUB_1:def 1;
A12: s1 \ s2 = ((a1 /\ b2) \ (b1 \/ a2)) \/
(a1 \ (b1 \/ a2 \/ b2)) \/ ((a1 /\ a2 /\ b2) \ b1) by A6,A7,Thm04;
A13: (a1 /\ b2) \ (b1 \/ a2) c= s1 \ s2 &
a1 \ (b1 \/ a2 \/ b2) c= s1 \ s2 &
(a1 /\ a2 /\ b2) \ b1 c= s1 \ s2
proof
A14: (a1 /\ b2) \ (b1 \/ a2) \/ (a1 \ (b1 \/ a2 \/ b2)) c= s1\s2
by A12,XBOOLE_1:7;
(a1 /\ b2) \ (b1 \/ a2) c= (a1 /\ b2) \ (b1 \/ a2) \/
(a1 \ (b1 \/ a2 \/ b2)) &
(a1 \ (b1 \/ a2 \/ b2)) c= (a1 /\ b2) \ (b1 \/ a2) \/
(a1 \ (b1 \/ a2 \/ b2)) by XBOOLE_1:7;
hence thesis by A12,A14,XBOOLE_1:7;
end;
per cases by A5,A12;
suppose
A16: ((a1 /\ b2) \ (b1 \/ a2)) <> {} &
(a1 \ (b1 \/ a2 \/ b2)) <> {} & ((a1 /\ a2 /\ b2) \ b1) <> {};
set x = {(a1 /\ b2) \ (b1 \/ a2),
a1 \ (b1 \/ a2 \/ b2),(a1 /\ a2 /\ b2) \ b1};
a17: x c= semidiff S
proof
let t be object;
assume t in x;
then t= (a1 /\ b2) \ (b1 \/ a2) or
t= a1 \ (b1 \/ a2 \/ b2) or
t=(a1 /\ a2 /\ b2) \ b1 by ENUMSET1:def 1;
hence t in semidiff S by A8,A10,A11,A9,SETFAM_1:def 6;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A18: t in x;
then reconsider t1=t as set;
t1 c= s1\s2 by A13,A18,ENUMSET1:def 1;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,Thm05;
let u be Subset of s1\s2;
assume
A19: u in x; then
A20: u= (a1 /\ b2) \ (b1 \/ a2) or
u= a1 \ (b1 \/ a2 \/ b2) or
u=(a1 /\ a2 /\ b2) \ b1 by ENUMSET1:def 1;
thus u <> {} by A19,A16;
let v be Subset of s1\s2;
assume v in x;
then v= (a1 /\ b2) \ (b1 \/ a2) or
v= a1 \ (b1 \/ a2 \/ b2) or
v= (a1 /\ a2 /\ b2) \ b1 by ENUMSET1:def 1;
hence u=v or u misses v by A20,Thm01;
end;
hence ex x be finite Subset of semidiff S st
x is a_partition of s1\s2 by a17;
end;
suppose
A20a: ((a1 /\ b2) \ (b1 \/ a2)) = {} &
(a1 \ (b1 \/ a2 \/ b2)) <> {} & ((a1 /\ a2 /\ b2) \ b1) <> {};
set x = {a1 \ (b1 \/ a2 \/ b2),
(a1 /\ a2 /\ b2) \ b1};
a21: x c= semidiff S
proof
let t be object;
assume t in x;
then t= a1 \ (b1 \/ a2 \/ b2) or
t=(a1 /\ a2 /\ b2) \ b1 by TARSKI:def 2;
hence t in semidiff S by A11,A9,SETFAM_1:def 6;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A22: t in x; then
reconsider t1=t as set;
a1 \ (b1 \/ a2 \/ b2) c= s1 \ s2 &
(a1 /\ a2 /\ b2) \ b1 c= s1 \ s2
proof
A23: (a1 /\ b2) \ (b1 \/ a2) \/ (a1 \ (b1 \/ a2 \/ b2)) c= s1\s2
by A12,XBOOLE_1:7;
(a1 /\ b2) \ (b1 \/ a2) c= (a1 /\ b2) \ (b1 \/ a2) \/
(a1 \ (b1 \/ a2 \/ b2)) &
(a1 \ (b1 \/ a2 \/ b2)) c= (a1 /\ b2) \ (b1 \/ a2) \/
(a1 \ (b1 \/ a2 \/ b2)) by XBOOLE_1:7;
hence thesis by A12,A23,XBOOLE_1:7;
end;
then t1 c= s1\s2 by A22,TARSKI:def 2;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,A20a,ZFMISC_1:75;
let u be Subset of s1\s2;
assume
A25: u in x; then
A26: u= a1 \ (b1 \/ a2 \/ b2) or
u=(a1 /\ a2 /\ b2) \ b1 by TARSKI:def 2;
thus u <> {} by A25,A20a;
let v be Subset of s1\s2;
assume v in x;
then v= a1 \ (b1 \/ a2 \/ b2) or
v= (a1 /\ a2 /\ b2) \ b1 by TARSKI:def 2;
hence u=v or u misses v by A26,Thm01;
end;
hence ex x be finite Subset of semidiff S st
x is a_partition of s1\s2 by a21;
end;
suppose
A26a: ((a1 /\ b2) \ (b1 \/ a2)) <> {} &
(a1 \ (b1 \/ a2 \/ b2)) <> {} & ((a1 /\ a2 /\ b2) \ b1) = {};
set x = {(a1 /\ b2) \ (b1 \/ a2),
a1 \ (b1 \/ a2 \/ b2)};
a27: x c= semidiff S
proof
let t be object;
assume t in x;
then t= (a1 /\ b2) \ (b1 \/ a2) or
t= a1 \ (b1 \/ a2 \/ b2) by TARSKI:def 2;
hence t in semidiff S by SETFAM_1:def 6,A8,A10,A11;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A28: t in x;
then reconsider t1=t as set;
t1 c= s1\s2 by A13,A28,TARSKI:def 2;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,A26a,ZFMISC_1:75;
let u be Subset of s1\s2;
assume
A29: u in x; then
A30: u= (a1 /\ b2) \ (b1 \/ a2) or
u= a1 \ (b1 \/ a2 \/ b2) by TARSKI:def 2;
thus u <> {} by A29,A26a;
let v be Subset of s1\s2;
assume v in x;
then v = (a1 /\ b2) \ (b1 \/ a2) or
v= a1 \ (b1 \/ a2 \/ b2) by TARSKI:def 2;
hence u=v or u misses v by A30,Thm01;
end;
hence ex x be finite Subset of semidiff S st
x is a_partition of s1\s2 by a27;
end;
suppose
A31: ((a1 /\ b2) \ (b1 \/ a2)) <> {} &
(a1 \ (b1 \/ a2 \/ b2)) = {} & ((a1 /\ a2 /\ b2) \ b1) <> {};
set x = {(a1 /\ b2) \ (b1 \/ a2), (a1 /\ a2 /\ b2) \ b1};
a32: x c= semidiff S
proof
let t be object;
assume t in x;
then t= (a1 /\ b2) \ (b1 \/ a2) or
t=(a1 /\ a2 /\ b2) \ b1 by TARSKI:def 2;
hence t in semidiff S by A8,A9,A10,SETFAM_1:def 6;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A33: t in x;
then reconsider t1=t as set;
t1 c= s1\s2 by A13,A33,TARSKI:def 2;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,A31,ZFMISC_1:75;
let u be Subset of s1\s2;
assume
A34: u in x; then
A35: u= (a1 /\ b2) \ (b1 \/ a2) or
u=(a1 /\ a2 /\ b2) \ b1 by TARSKI:def 2;
thus u <> {} by A31,A34;
let v be Subset of s1\s2;
assume v in x;
then v= (a1 /\ b2) \ (b1 \/ a2) or
v= (a1 /\ a2 /\ b2) \ b1 by TARSKI:def 2;
hence u=v or u misses v by A35,Thm01;
end;
hence ex x be finite Subset of semidiff S st
x is a_partition of s1\s2 by a32;
end;
suppose
A36: ((a1 /\ b2) \ (b1 \/ a2)) <> {} &
(a1 \ (b1 \/ a2 \/ b2)) = {} & ((a1 /\ a2 /\ b2) \ b1) = {};
set x = {(a1 /\ b2) \ (b1 \/ a2)};
a37: x c= semidiff S
proof
let t be object;
assume t in x;
then t= (a1 /\ b2) \ (b1 \/ a2) by TARSKI:def 1;
hence t in semidiff S by SETFAM_1:def 6,A8,A10;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A38: t in x;
then reconsider t1=t as set;
t1 c= s1\s2 by A13,A38,TARSKI:def 1;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,A36;
let u be Subset of s1\s2;
assume
A39: u in x; then
A40: u= (a1 /\ b2) \ (b1 \/ a2) by TARSKI:def 1;
thus u <> {} by A39,A36;
thus for v be Subset of s1\s2 st v in x holds u=v or u misses v
by A40,TARSKI:def 1;
end;
hence ex x be finite Subset of semidiff S st
x is a_partition of s1\s2 by a37;
end;
suppose
A41: ((a1 /\ b2) \ (b1 \/ a2)) = {} &
(a1 \ (b1 \/ a2 \/ b2)) <> {} & ((a1 /\ a2 /\ b2) \ b1) = {};
set x = {a1 \ (b1 \/ a2 \/ b2)};
a42: x c= semidiff S
proof
let t be object;
assume t in x;
then t= a1 \ (b1 \/ a2 \/ b2) by TARSKI:def 1;
hence t in semidiff S by SETFAM_1:def 6,A11;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A43: t in x;
then reconsider t1=t as set;
t1 c= s1\s2 by A13,A43,TARSKI:def 1;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,A41;
let u be Subset of s1\s2;
assume
A44: u in x; then
A45: u= a1 \ (b1 \/ a2 \/ b2) by TARSKI:def 1;
thus u <> {} by A44,A41;
thus for v be Subset of s1\s2 st v in x holds u=v or u misses v
by A45,TARSKI:def 1;
end;
hence ex x be finite Subset of semidiff S st
x is a_partition of s1\s2 by a42;
end;
suppose
A46: ((a1 /\ b2) \ (b1 \/ a2)) = {} &
(a1 \ (b1 \/ a2 \/ b2)) = {} & ((a1 /\ a2 /\ b2) \ b1) <> {};
set x = {(a1 /\ a2 /\ b2) \ b1};
a47: x c= semidiff S
proof
let t be object;
assume t in x;
then t=(a1 /\ a2 /\ b2) \ b1 by TARSKI:def 1;
hence t in semidiff S by SETFAM_1:def 6,A9;
end;
x c= bool (s1\s2)
proof
let t be object;
assume
A48: t in x;
then reconsider t1=t as set;
t1 c= s1\s2 by A13,A48,TARSKI:def 1;
hence t in bool (s1\s2);
end;
then reconsider x as Subset-Family of s1\s2;
x is a_partition of s1\s2
proof
thus union x = s1\s2 by A12,A46;
let u be Subset of s1\s2;
assume
A49: u in x; then
A50: u=(a1 /\ a2 /\ b2) \ b1 by TARSKI:def 1;
thus u <> {} by A49,A46;
thus for v be Subset of s1\s2 st v in x holds u=v or u misses v
by A50,TARSKI:def 1;
end;
hence ex x be finite Subset of semidiff S st x is a_partition of s1\s2
by a47;
end;
end;
end;
registration
let X be set,
S be with_empty_element cap-closed cup-closed Subset-Family of X;
cluster semidiff S -> cap-closed diff-finite-partition-closed;
coherence by Thm14;
end;
theorem
for X being set,
S being with_empty_element cap-closed cup-closed Subset-Family of X holds
semidiff S is semiring_of_sets of X;
begin :: Classical Semiring of Sets and Topological Space
definition
let T be non empty TopSpace;
func capOpCl T -> Subset-Family of [#]T equals
{A /\ B where A, B is Subset of T: A is open & B is closed};
coherence
proof
{A /\ B where A, B is Subset of T:
A is open & B is closed} c= bool [#]T
proof
let t be object;
assume t in {A /\ B where A, B is Subset of T: A is open & B is closed};
then consider A0,B0 be Subset of T such that
A1: t=A0/\B0 and
A0 is open and
B0 is closed;
reconsider t0=t as set by A1;
[#]T is non empty & A0 is Subset of [#]T & B0 is Subset of [#]T
by STRUCT_0:def 3;
then t0 c= [#]T /\ [#]T by A1,XBOOLE_1:27;
hence t in bool [#]T;
end;
hence thesis;
end;
end;
:: T being Topology
:: { O1 \ O2 : O1 is open, O2 is open} is classical semiring of sets
Thm15:
for T being non empty TopSpace holds
capOpCl T is with_empty_element cap-closed diff-finite-partition-closed
proof
let T be non empty TopSpace;
set SR={A /\ B where A, B is Subset of T: A is open & B is closed};
the topology of T is
with_empty_element cap-closed cup-closed Subset-Family of [#]T
proof
A1: the topology of T is with_empty_element by PRE_TOPC:1;
A2: the topology of T is cap-closed by PRE_TOPC:def 1;
the topology of T is cup-closed
proof
now
let x,y be set;
assume
A3: x in the topology of T & y in the topology of T;
{x,y} c= bool the carrier of T
proof
let t be object;
assume t in {x,y};
then t in the topology of T by A3,TARSKI:def 2;
hence t in bool the carrier of T;
end;
then reconsider xy={x,y} as Subset-Family of T;
xy c= the topology of T by A3,TARSKI:def 2;
then union xy in the topology of T by PRE_TOPC:def 1;
hence x \/ y in the topology of T by ZFMISC_1:75;
end;
hence thesis;
end;
hence thesis by A1,A2,STRUCT_0:def 3;
end;
then reconsider XS=the topology of T as
with_empty_element cap-closed cup-closed Subset-Family of [#]T;
SR=semidiff XS
proof
hereby
let x be object;
assume x in SR;
then consider A,B be Subset of T such that
A4: x = A /\ B and
A5: A is open and
A6: B is closed;
A is Element of bool [#]T by STRUCT_0:def 3;
then
A7: A \ [#]T is empty by XBOOLE_1:37;
A8: A \ ([#]T \ B) = (A \ [#]T) \/ (A /\ B) by XBOOLE_1:52
.=A /\ B by A7;
reconsider A1=A,CB1=[#]T \ B as Element of XS
by A5,A6,PRE_TOPC:def 2,PRE_TOPC:def 3;
x = A1 \ CB1 by A4,A8;
hence x in semidiff XS by SETFAM_1:def 6;
end;
let x be object;
assume x in semidiff XS;
then consider A,B be Element of XS such that
A9: x = A \ B by LemX1;
A in the topology of T & B in the topology of T;
then reconsider A1=A,B1=B as Subset of T;
A10: A1 \ [#]T is empty & [#]T /\ B1 = B1 by XBOOLE_1:37,XBOOLE_1:28;
A11: A1 is open & B1 is open by PRE_TOPC:def 2;
A12: [#]T \ ([#]T \ B1) = [#]T /\ B1 by XBOOLE_1:48
.= B1 by XBOOLE_1:28; then
A13: [#]T \ B1 is closed by PRE_TOPC:def 2,PRE_TOPC:def 3;
A1 \ ([#]T \ ([#]T \ B1))
= (A1 \ [#]T) \/ (A1 /\ ([#]T \ B1)) by XBOOLE_1:52
.= A1 /\ ([#]T \ B1) by A10;
hence x in SR by A9,A11,A12,A13;
end;
hence thesis;
end;
registration
let T be non empty TopSpace;
cluster capOpCl T -> with_empty_element cap-closed
diff-finite-partition-closed;
coherence by Thm15;
end;
:: T being Topology
:: { O1 \ O2 : O1 is open, O2 is open} is semiring of sets
theorem
for T being non empty TopSpace holds capOpCl T is semiring_of_sets of [#]T;
begin :: Finite Product of SemiringFamily of Sets
registration
let n be Nat;
cluster non-empty for n-element FinSequence;
existence
proof
set p = (n |-> {{}});
take p;
not {} in rng p
proof
assume {} in rng p;
then consider a be object such that
A1: a in dom p and
A2: {} = p.a by FUNCT_1:def 3;
a in Seg n by FINSEQ_1:89,A1;
hence contradiction by A2,FINSEQ_2:57;
end;
hence thesis by RELAT_1:def 9;
end;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
mode SemiringFamily of X -> n-element FinSequence means
:Def2:
for i being Nat st i in Seg n holds
it.i is semiring_of_sets of X.i;
existence
proof
deffunc F(set)=Fin (X.$1);
consider p being FinSequence such that
A1: len p = n and
A2: for i being Nat st i in dom p holds p.i=F(i) from FINSEQ_1:sch 2;
reconsider p as n-element FinSequence by A1,CARD_1:def 7;
take p;
let i be Nat;
assume
A3: i in Seg n;
reconsider Xi=X.i as set;
A4: Fin Xi is semiring_of_sets of Xi by SRINGS_2:6;
i in dom p by A3,A1,FINSEQ_1:def 3;
hence p.i is semiring_of_sets of X.i by A2,A4;
end;
end;
reserve n for non zero Nat;
reserve X for non-empty n-element FinSequence;
theorem Thm16:
for S being SemiringFamily of X holds dom S = dom X
proof
let S be SemiringFamily of X;
dom S = Seg n by FINSEQ_1:89;
hence thesis by FINSEQ_1:89;
end;
theorem Thm17:
for S being SemiringFamily of X holds
for i be Nat st i in Seg n holds union (S.i) c= X.i
proof
let S be SemiringFamily of X;
let i be Nat;
assume i in Seg n;
then S.i is semiring_of_sets of X.i by Def2;
then union (S.i) c= union bool (X.i) by ZFMISC_1:77;
hence union (S.i) c= X.i by ZFMISC_1:81;
end;
theorem Thm18:
for f being Function, X be n-element FinSequence st f in product X holds
f is n-element FinSequence
proof
let f be Function, X be n-element FinSequence;
assume
A1: f in product X;
A2: dom X = Seg n by FINSEQ_1:89;
then dom f = Seg n by A1,CARD_3:9;
then reconsider f as FinSequence by FINSEQ_1:def 2;
dom f is n-element by A1,A2,CARD_3:9;
then card dom f = n by CARD_1:def 7;
then card f = n by CARD_1:62;
hence thesis by CARD_1:def 7;
end;
definition
let n be non zero Nat, X be n-element FinSequence;
func SemiringProduct(X) -> set means :Def3:
for f being object holds f in it iff
ex g being Function st f = product g & g in product X;
existence
proof
defpred P[object] means
ex g be Function st $1 = product g & g in product X;
consider Y be set such that
A1: for x being object holds
x in Y iff x in bool Funcs(dom X, union Union X ) & P[x]
from XBOOLE_0:sch 1;
take Y;
now
thus for x be object st x in Y holds
ex g be Function st x = product g & g in product X by A1;
let x be object;
assume
A2: ex g be Function st x = product g & g in product X;
given g be Function such that
A3: x = product g and
A4: g in product X;
A5: dom g = dom X by A4,CARD_3:9;
rng g c= Union X
proof
let t be object;
assume t in rng g;
then consider u be object such that
A6: u in dom g and
A7: t=g.u by FUNCT_1:def 3;
consider h be Function such that
A8: g = h and
A9: dom h = dom X and
A10: for v be object st v in dom X holds h.v in X.v by A4,CARD_3:def 5;
t in X.u & X.u in rng X by A8,A9,A10,A6,A7,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then Union g c= union Union X by ZFMISC_1:77;
then Funcs(dom g,Union g) c= Funcs(dom X, union Union X)
by A5,FUNCT_5:56; then
A11: bool Funcs(dom g,Union g) c= bool Funcs(dom X, union Union X)
by ZFMISC_1:67;
product g c= Funcs(dom g, Union g) by FUNCT_6:1;
hence x in Y by A2,A1,A3,A11;
end;
hence thesis;
end;
uniqueness
proof
let S1,S2 be set such that
A12:for f being object holds f in S1 iff
ex g being Function st f = product g & g in product X and
A13:for f being object holds f in S2 iff
ex g being Function st f = product g & g in product X;
now
let x be object;
x in S1 iff
ex g being Function st x = product g & g in product X by A12;
hence x in S1 iff x in S2 by A13;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Thm19:
for X being n-element FinSequence holds
SemiringProduct(X) c= bool Funcs(dom X, union Union X)
proof
let X be n-element FinSequence;
let x be object;
assume x in SemiringProduct(X);
then consider g be Function such that
A1: x = product g and
A2: g in product X by Def3;
A3: dom g = dom X by A2,CARD_3:9;
rng g c= Union X
proof
let t be object;
assume t in rng g;
then consider u be object such that
A4: u in dom g and
A5: t=g.u by FUNCT_1:def 3;
consider h be Function such that
A6: g = h and
A7: dom h = dom X and
A8: for v be object st v in dom X holds h.v in X.v by A2,CARD_3:def 5;
t in X.u & X.u in rng X by A6,A7,A8,A4,A5,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then Union g c= union Union X by ZFMISC_1:77;
then Funcs(dom g,Union g) c= Funcs(dom X, union Union X)
by A3,FUNCT_5:56; then
A9: bool Funcs(dom g,Union g) c= bool Funcs(dom X, union Union X)
by ZFMISC_1:67;
product g c= Funcs(dom g, Union g) by FUNCT_6:1;
hence thesis by A1,A9;
end;
theorem Thm20:
for S being SemiringFamily of X holds
SemiringProduct(S) is Subset-Family of product X
proof
let S be SemiringFamily of X;
reconsider SPS=SemiringProduct(S) as Subset of
bool Funcs(dom S,union Union S) by Thm19;
SPS c= bool product X
proof
let x be object;
assume
A1: x in SPS;
reconsider x1=x as set by TARSKI:1;
x1 c= product X
proof
let t be object;
assume
A2: t in x1;
consider g be Function such that
A3: x1 = product g and
A4: g in product S by A1,Def3;
A5: dom g = dom S by A4,CARD_3:9;
consider u be Function such that
A7: t=u and
A8: dom u = dom g and
A9: for v be object st v in dom g holds u.v in g.v by A2,A3,CARD_3:def 5;
consider w be Function such that
A10: g=w and
dom w = dom S and
A12: for y be object st y in dom S holds w.y in S.y by A4,CARD_3:def 5;
A12a: dom S = dom X by Thm16;
now
let a be object;
assume
A13: a in dom X;
A15: a in Seg n by A13,FINSEQ_1:89;
reconsider a1=a as Nat by A13;
u.a in g.a & g.a in S.a by A13,A12a,A10,A12,A9,A5;
then
A16: u.a in union (S.a) & a in Seg n by A13,FINSEQ_1:89,TARSKI:def 4;
union (S.a) c= X.a by A15,Thm17;
hence u.a in X.a by A16;
end;
hence t in product X by A12a,A5,A8,A7,CARD_3:def 5;
end;
hence x in bool product X;
end;
hence thesis;
end;
theorem Thm21:
for X being non-empty 1-element FinSequence holds
product X = the set of all <*x*> where x is Element of X.1
proof
let X be non-empty 1-element FinSequence;
A1: dom X = {1} by FINSEQ_1:89,FINSEQ_1:2;
A2: X.1 is non empty
proof
assume
A3: X.1 is empty;
1 in dom X by A1,TARSKI:def 1;
hence contradiction by A3;
end;
len X = 1 by CARD_1:def 7; then
X = <*X.1*> by FINSEQ_1:40; then
consider I be Function of X.1, product X such that
I is one-to-one and
A4: I is onto and
A5: for x be object st x in X.1 holds I.x = <*x*> by A2,PRVECT_3:4;
now
hereby
let t be object;
assume t in product X;
then t in rng I by A4,FUNCT_2:def 3;
then consider a be object such that
A6: a in dom I and
A7: t = I.a by FUNCT_1:def 3;
t = <*a*> by A7,A6,A5;
hence t in the set of all <*x*> where x is Element of X.1 by A6;
end;
let t be object;
assume t in the set of all <*x*> where x is Element of X.1;
then consider x be Element of X.1 such that
A9: t = <*x*>;
reconsider t1=t as FinSequence by A9;
dom t1 = Seg 1 by A9,FINSEQ_1:def 8;
then
A10: dom t1 = dom X by FINSEQ_1:89;
for a be object st a in dom X holds t1.a in X.a
proof
let a be object;
assume a in dom X;
then
A11: a = 1 by A1,TARSKI:def 1;
then t1.a is Element of X.1 by A9;
hence thesis by A2,A11;
end;
hence t in product X by A10,CARD_3:def 5;
end;
then the set of all <*x*> where x is Element of X.1 c= product X &
product X c= the set of all <*x*> where x is Element of X.1;
hence thesis;
end;
Thm22:
product <*{}*> is empty
proof
{} in {{}} by TARSKI:def 1;
then {} in rng<*{}*> by FINSEQ_1:39;
hence thesis by CARD_3:26;
end;
registration
cluster product <*{}*> -> empty;
coherence by Thm22;
end;
theorem Thm23:
for x be non empty set holds
product <*x*> = the set of all <*y*> where y is Element of x
proof
let x be non empty set;
A1: rng <*x*> = {x} & <*x*>.1 = x by FINSEQ_1:38; then
{} in rng <*x*> implies {} = x; then
<*x*> is non-empty 1-element FinSequence by RELAT_1:def 9;
hence thesis by A1,Thm21;
end;
theorem Thm24:
for X being non-empty 1-element FinSequence, S being SemiringFamily of X
holds
SemiringProduct(S)=the set of all product <*s*> where s is Element of S.1
proof
let X be non-empty 1-element FinSequence,
S be SemiringFamily of X;
A1: dom X = {1} by FINSEQ_1:2,FINSEQ_1:89;
A2: S is non-empty
proof
assume not S is non-empty;
then {} in rng S by RELAT_1:def 9;
then consider a be object such that
A3: a in dom S and
A4: S.a = {} by FUNCT_1:def 3;
a in dom X by Thm16,A3; then
A5: S.1 = {} by A4,A1,TARSKI:def 1;
S is SemiringFamily of X & 1 in Seg 1 by FINSEQ_1:3;
hence contradiction by A5,Def2;
end;
then
A6: product S = the set of all <*s*> where s is Element of S.1 by Thm21;
now
hereby
let x be object;
assume x in SemiringProduct(S);
then consider f be Function such that
A7: x = product f and
A8: f in product S by Def3;
f in the set of all <*s*> where s is Element of S.1 by A2,A8,Thm21;
then consider s be Element of S.1 such that
A9: f = <*s*>;
thus x in the set of all product <*s*> where
s is Element of S.1 by A7,A9;
end;
let x be object;
assume x in the set of all product <*s*> where s is Element of S.1;
then consider s be Element of S.1 such that
A10: x = product <*s*>;
set f = <*s*>;
x = product f & f in product S by A10,A6;
hence x in SemiringProduct(S) by Def3;
end;
then the set of all product <*s*> where
s is Element of S.1 c= SemiringProduct(S) &
SemiringProduct(S) c= the set of all product <*s*> where
s is Element of S.1;
hence thesis;
end;
theorem Thm25:
for x,y being set holds
product <*x*> /\ product <*y*> = product <*(x/\y)*>
proof
let x,y be set;
per cases;
suppose
A1: not x is empty & not y is empty & not x/\y is empty;
then
A2: product <*x*> = the set of all <*t*> where t is Element of x &
product <*y*> = the set of all <*t*> where t is Element of y &
product <*(x/\y)*> = the set of all <*t*> where
t is Element of x/\y by Thm23;
set Px = the set of all <*t*> where t is Element of x;
set Py = the set of all <*t*> where t is Element of y;
set Pxy = the set of all <*t*> where t is Element of x/\y;
now
hereby
let u be object;
assume u in Px/\Py;
then
A3: u in Px & u in Py by XBOOLE_0:def 4;
then consider ux be Element of x such that
A4: u=<*ux*>;
consider uy be Element of y such that
A5: u=<*uy*> by A3;
ux=uy by A4,A5,FINSEQ_1:76;
then ux in x/\y by A1,XBOOLE_0:def 4;
hence u in Pxy by A4;
end;
let u be object;
assume u in Pxy;
then consider uxy be Element of x/\y such that
A6: u = <*uxy*>;
uxy is Element of x & uxy is Element of y by A1,XBOOLE_0:def 4;
then u in Px & u in Py by A6;
hence u in Px/\Py by XBOOLE_0:def 4;
end;
then Px/\Py c= Pxy & Pxy c= Px/\Py;
hence thesis by A2;
end;
suppose
A7: not x is empty & not y is empty & x/\y is empty; then
A8: product <*x*> = the set of all <*t*> where t is Element of x &
product <*y*> = the set of all <*t*> where t is Element of y by Thm23;
set Px = the set of all <*t*> where t is Element of x;
set Py = the set of all <*t*> where t is Element of y;
Px /\ Py c= {}
proof
let t be object;
assume t in Px /\ Py;
then
A9: t in Px & t in Py by XBOOLE_0:def 4;
then consider t1 be Element of x such that
A10: t=<*t1*>;
consider t2 be Element of y such that
A11: t=<*t2*> by A9;
t1=t2 by A10,A11,FINSEQ_1:76;
hence thesis by A7,XBOOLE_0:def 4;
end;
hence thesis by A8,A7;
end;
suppose
x is empty or y is empty;
hence thesis by Thm22;
end;
end;
theorem Thm26:
for x,y being set holds product <*x*> \ product <*y*> = product <*(x\y)*>
proof
let x,y be set;
per cases;
suppose
A1: not x is empty & not y is empty & not x\y is empty;
then
A2: product <*x*> = the set of all <*t*> where t is Element of x &
product <*y*> = the set of all <*t*> where t is Element of y &
product <*(x\y)*> = the set of all <*t*> where t is Element of x\y
by Thm23;
set Px = the set of all <*t*> where t is Element of x;
set Py = the set of all <*t*> where t is Element of y;
set Pxy = the set of all <*t*> where t is Element of x\y;
now
hereby
let u be object;
assume u in Px\Py;
then
A3: u in Px & not u in Py by XBOOLE_0:def 5;
then consider ux be Element of x such that
A4: u=<*ux*>;
not ux in y by A3,A4;
then ux in x\y by A1,XBOOLE_0:def 5;
hence u in Pxy by A4;
end;
let u be object;
assume u in Pxy;
then consider uxy be Element of x\y such that
A5: u = <*uxy*>;
A6: uxy is Element of x & not uxy is Element of y by A1,XBOOLE_0:def 5;
now
assume u in Py;
then consider a be Element of y such that
A7: <*uxy*> = <*a*> by A5;
thus contradiction by A7,A6,FINSEQ_1:76;
end;
then u in Px & not u in Py by A5,A6;
hence u in Px\Py by XBOOLE_0:def 5;
end;
then Px\Py c= Pxy & Pxy c= Px\Py;
hence thesis by A2;
end;
suppose
A8: not x is empty & not y is empty & x\y is empty;
then
A9: product <*x*> = the set of all <*t*> where t is Element of x &
product <*y*> = the set of all <*t*> where t is Element of y by Thm23;
set Px = the set of all <*t*> where t is Element of x;
set Py = the set of all <*t*> where t is Element of y;
Px \ Py c= {}
proof
let t be object;
assume t in Px \ Py; then
A10: t in Px & not t in Py by XBOOLE_0:def 5;
then consider t1 be Element of x such that
A11: t=<*t1*>;
not t1 in y by A10,A11;
hence thesis by A8,XBOOLE_0:def 5;
end;
hence thesis by A8,A9;
end;
suppose
x is empty or y is empty;
hence thesis by Thm22;
end;
end;
theorem Thm27:
for X being non-empty 1-element FinSequence,
S being SemiringFamily of X holds
the set of all product <*s*> where s is Element of S.1 is
semiring_of_sets of the set of all <*x*> where x is Element of X.1
proof
let X be non-empty 1-element FinSequence, S be SemiringFamily of X;
S is SemiringFamily of X & 1 in Seg 1 by FINSEQ_1:3;
then
A1: S.1 is semiring_of_sets of X.1 by Def2;
set S1=the set of all product <*s*> where s is Element of S.1;
set X1=the set of all <*x*> where x is Element of X.1;
now
S1 c= bool X1
proof
let x be object;
assume
A2: x in S1;
then consider s0 be Element of S.1 such that
A3: x = product <*s0*>;
per cases;
suppose
A4: s0 is non empty;
reconsider x1=x as set by A2;
x1 c= X1
proof
let y be object;
assume
y in x1;
then y in the set of all <*a*> where a is Element of s0
by A3,A4,Thm23;
then consider a be Element of s0 such that
A6: y = <*a*>;
A7: a in union (S.1) by A4,A1,TARSKI:def 4;
union (S.1) c= union bool (X.1) by A1,ZFMISC_1:77;
then union (S.1) c= (X.1) by ZFMISC_1:81;
hence y in X1 by A6,A7;
end;
hence x in bool X1;
end;
suppose
A8: s0 is empty;
product <*{}*> c= X1;
hence x in bool X1 by A8,A3;
end;
end;
then reconsider S2=S1 as Subset-Family of X1;
now
Z: {} is Element of S.1 by A1,SETFAM_1:def 8; then
A9: {} in S1 by Thm22;
thus S2 is with_empty_element by Z,Thm22;
now
let s1,s2 be Element of S2;
assume
A10: s1/\s2 is non empty;
A11: s1 in S1 & s2 in S2 by A9;
then consider sa1 be Element of S.1 such that
A12: s1 = product <*sa1*>;
consider sa2 be Element of S.1 such that
A13: s2 = product <*sa2*> by A11;
A14: sa1/\sa2 is non empty by A12,A13,A10,Thm25,Thm22;
then consider ax be finite Subset of S.1 such that
A15: ax is a_partition of sa1/\sa2 by A1,SRINGS_1:def 1;
A16: ax is non empty by A14,A15;
set x = the set of all product <*t*> where t is Element of ax;
now
deffunc F(object) = product <*$1*>;
consider f being Function such that
A17: dom f = ax and
A18: for x be object st x in ax holds f.x=F(x) from FUNCT_1:sch 3;
rng f = x
proof
now
hereby
let t be object;
assume t in rng f;
then consider q be object such that
A19: q in dom f and
A20: t = f.q by FUNCT_1:def 3;
t = F(q) by A17,A19,A20,A18;
hence t in x by A17,A19;
end;
let t be object;
assume t in x;
then consider u be Element of ax such that
A21: t= product <*u*>;
f.u = F(u) by A18,A14,A15;
hence t in rng f by A21,A17,A14,A15,FUNCT_1:def 3;
end;
then x c= rng f & rng f c= x;
hence thesis;
end;
hence x is finite by A17,FINSET_1:8;
x c= S2
proof
let t be object;
assume t in x;
then consider u be Element of ax such that
A22: t = product <*u*>;
u in ax & ax c= S.1 by A16;
hence t in S2 by A22;
end;
hence x is Subset of S2;
now
A23: x c= bool (s1/\s2)
proof
let t be object;
assume
t in x;
then consider u0 be Element of ax such that
A24: t = product <*u0*>;
reconsider t1=t as set by A24;
per cases;
suppose
A25: t1 is empty;
{} c= (s1/\s2);
hence thesis by A25;
end;
suppose
A26: t1 is non empty; then
A28: t = the set of all <*y*> where y is Element of u0
by A24,Thm22,Thm23;
t1 c= s1/\s2
proof
let y be object;
assume y in t1;
then consider z be Element of u0 such that
A29: y=<*z*> by A28;
A30: product<*sa1/\sa2*> = the set of all <*a*> where
a is Element of sa1/\sa2 by A14,Thm23;
u0 in ax & union ax = sa1/\sa2 by A16,A15,EQREL_1:def 4;
then z in sa1/\sa2 by A24,A26,Thm22,TARSKI:def 4;
then y in product <*sa1/\sa2*> by A29,A30;
hence y in s1/\s2 by A12,A13,Thm25;
end;
hence thesis;
end;
end;
hence x is Subset-Family of s1/\s2;
now
hereby
let a be object;
assume a in union x;
then consider b be set such that
A31: a in b and
A32: b in x by TARSKI:def 4;
thus a in s1/\s2 by A31,A32,A23;
end;
let a be object;
assume a in s1/\s2; then
A33: a in product <*sa1/\sa2*> by A12,A13,Thm25;
product <*sa1/\sa2*> = the set of all <*u*> where
u is Element of sa1/\sa2 by A14,Thm23;
then consider b be Element of sa1/\sa2 such that
A34: a = <*b*> by A33;
b in sa1/\sa2 & union ax = sa1/\sa2 by A14,A15,EQREL_1:def 4;
then consider d be set such that
A35: b in d & d in ax by TARSKI:def 4;
A36: product <*d*> = the set of all <*u*> where
u is Element of d by A35,Thm23;
<*b*> in product <*d*> & product <*d*> in x by A35,A36;
hence a in union x by A34,TARSKI:def 4;
end;
then union x c= s1/\s2 & s1/\s2 c= union x;
hence union x = s1/\s2;
hereby
let A be Subset of s1/\s2;
assume A in x;
then consider a be Element of ax such that
A37: A = product <*a*>;
A38: a in ax by A16;
A39: A = the set of all <*u*> where u is Element of a
by A14,A15,A37,Thm23;
consider b be object such that
A40: b in a by A14,A15,XBOOLE_0:def 1;
<*b*> in A by A39,A40;
hence A<>{};
let B be Subset of s1/\s2;
assume B in x;
then consider b be Element of ax such that
A41: B = product <*b*>;
A42: b in ax by A16;
a misses b implies A misses B by A37,A41,Thm25,Thm22;
hence A=B or A misses B by A42,A38,A15,EQREL_1:def 4,A37,A41;
end;
end;
hence x is a_partition of s1/\s2 by EQREL_1:def 4;
end;
hence ex x be finite Subset of S2 st
x is a_partition of s1/\s2;
end;
hence S2 is cap-finite-partition-closed;
now
let s1,s2 be Element of S2;
assume
A44: s2 c= s1;
per cases;
suppose
A45: s1\s2 is empty;
now
{} c= S2;
hence {} is finite Subset of S2;
thus {} is a_partition of {} by EQREL_1:45;
end;
hence ex x be finite Subset of S2 st
x is a_partition of s1\s2 by A45;
end;
suppose
A46: s1\s2 is non empty & s2 is empty;
now
{s1} c= S2
proof
let t be object;
assume t in {s1};
then t = s1 by TARSKI:def 1;
hence thesis by A9;
end;
hence {s1} is finite Subset of S2;
thus {s1} is a_partition of s1 by A46,EQREL_1:39;
end;
hence ex x be finite Subset of S2 st
x is a_partition of s1\s2 by A46;
end;
suppose
A47: s1\s2 is non empty & s2 is non empty;
A48: s1 in S1 & s2 in S2 by A9;
then consider sa1 be Element of S.1 such that
A49: s1 = product <*sa1*>;
consider sa2 be Element of S.1 such that
A50: s2 = product <*sa2*> by A48;
A51: sa1 is non empty by A47,A49;
A52: product <*sa1*> = the set of all <*u*> where
u is Element of sa1 by A47,A49,Thm22,Thm23;
A53: product <*sa2*> = the set of all <*u*> where
u is Element of sa2 by A47,A50,Thm22,Thm23;
sa2 c= sa1
proof
assume not sa2 c= sa1;
then consider a be object such that
A54: a in sa2 and
A55: not a in sa1;
<*a*> in s2 by A50,A54,A53;
then <*a*> in product <*sa1*> by A44,A49;
then consider a0 be Element of sa1 such that
A56: <*a*> = <*a0*> by A52;
a=a0 by A56,FINSEQ_1:76;
hence contradiction by A51,A55;
end;
then consider ax be finite Subset of S.1 such that
A57: ax is a_partition of sa1\sa2 by A1,SRINGS_1:def 3;
A58: ax is non empty
proof
assume ax is empty;
then sa1 \ sa2 = {} by A57;
hence contradiction by A47,A49,A50,Thm26,Thm22;
end;
A59: sa1\sa2 <> {} by A49,A50,A47,Thm26,Thm22;
set x = the set of all product <*t*> where t is Element of ax;
now
deffunc F(object) = product <*$1*>;
consider f being Function such that
A60: dom f = ax and
A61: for x be object st x in ax holds f.x=F(x) from FUNCT_1:sch 3;
rng f = x
proof
now
hereby
let t be object;
assume t in rng f;
then consider q be object such that
A62: q in dom f and
A63: t = f.q by FUNCT_1:def 3;
t = product <*q*> & q in ax by A60,A61,A62,A63;
hence t in x;
end;
let t be object;
assume t in x;
then consider u be Element of ax such that
A64: t= product <*u*>;
f.u = F(u) by A61,A58;
hence t in rng f by A64,A60,A58,FUNCT_1:def 3;
end;
then x c= rng f & rng f c= x;
hence thesis;
end;
hence x is finite by A60,FINSET_1:8;
x c= S2
proof
let t be object;
assume t in x;
then consider u be Element of ax such that
A65: t = product <*u*>;
u in ax & ax c= S.1 by A58;
hence t in S2 by A65;
end;
hence x is Subset of S2;
now
A66: x c= bool (s1\s2)
proof
let t be object;
assume
t in x;
then consider u0 be Element of ax such that
A67: t = product <*u0*>;
reconsider t1=t as set by A67;
per cases;
suppose
A68: t1 is empty;
{} c= (s1\s2);
hence thesis by A68;
end;
suppose
A69: t1 is non empty; then
A71: t = the set of all <*y*> where y is Element of u0
by A67,Thm22,Thm23;
t1 c= s1\s2
proof
let y be object;
assume y in t1;
then consider z be Element of u0 such that
A72: y=<*z*> by A71;
A73: product<*sa1\sa2*> = the set of all <*a*> where
a is Element of sa1\sa2 by A59,Thm23;
u0 in ax & union ax = sa1\sa2 by A57,A58,EQREL_1:def 4;
then z in sa1\sa2 by A67,A69,Thm22,TARSKI:def 4;
then y in product <*sa1\sa2*> by A72,A73;
hence y in s1\s2 by A49,A50,Thm26;
end;
hence thesis;
end;
end;
hence x is Subset-Family of s1\s2;
now
hereby
let a be object;
assume a in union x;
then consider b be set such that
A74: a in b and
A75: b in x by TARSKI:def 4;
thus a in s1\s2 by A66,A74,A75;
end;
let a be object;
assume
A76: a in s1\s2;
A77: a in product <*sa1\sa2*> by Thm26,A76,A49,A50;
product <*sa1\sa2*> = the set of all <*u*> where
u is Element of sa1\sa2 by A59,Thm23;
then consider b be Element of sa1\sa2 such that
A78: a = <*b*> by A77;
b in sa1\sa2 & union ax = sa1\sa2 by A59,A57,EQREL_1:def 4;
then consider d be set such that
A79: b in d & d in ax by TARSKI:def 4;
A80: product <*d*> = the set of all <*u*> where
u is Element of d by Thm23,A79;
<*b*> in product <*d*> & product <*d*> in x by A79,A80;
hence a in union x by A78,TARSKI:def 4;
end;
then union x c= s1\s2 & s1\s2 c= union x;
hence union x = s1\s2;
hereby
let A be Subset of s1\s2;
assume A in x;
then consider a be Element of ax such that
A81: A = product <*a*>;
A82: a in ax by A58;
A83: A = the set of all <*u*> where u is Element of a
by A57,A58,A81,Thm23;
consider b be object such that
A84: b in a by A57,A58,XBOOLE_0:def 1;
<*b*> in A by A83,A84;
hence A<>{};
let B be Subset of s1\s2;
assume B in x;
then consider b be Element of ax such that
A85: B = product <*b*>;
A86: b in ax by A58;
a misses b implies A misses B by A81,A85,Thm25,Thm22;
hence A=B or A misses B
by A86,A81,A85,A82,A57,EQREL_1:def 4;
end;
end;
hence x is a_partition of s1\s2 by EQREL_1:def 4;
end;
hence ex x be finite Subset of S2 st
x is a_partition of s1\s2;
end;
end;
hence S2 is diff-c=-finite-partition-closed;
end;
hence S1 is semiring_of_sets of X1;
end;
hence thesis;
end;
theorem Thm28:
for X being non-empty 1-element FinSequence, S being SemiringFamily of X
holds SemiringProduct(S) is semiring_of_sets of product X
proof
let X be non-empty 1-element FinSequence, S be SemiringFamily of X;
set S1=the set of all product <*s*> where s is Element of S.1;
set X1=the set of all <*x*> where x is Element of X.1;
S1 = SemiringProduct(S) & X1 = product X by Thm21,Thm24;
hence thesis by Thm27;
end;
theorem Thm29:
for X1,X2 being set, S1 being semiring_of_sets of X1,
S2 being semiring_of_sets of X2 holds
the set of all [:s1,s2:] where s1 is Element of S1,
s2 is Element of S2 is semiring_of_sets of [:X1,X2:]
proof
let X1,X2 be set, S1 be semiring_of_sets of X1,
S2 be semiring_of_sets of X2;
set S = {s where s is Subset of [:X1,X2:]:ex x1,x2 be set st x1 in S1 &
x2 in S2 & s=[:x1,x2:]};
S is semiring_of_sets of [:X1,X2:] by SRINGS_2:7;
hence thesis by SRINGS_2:2;
end;
theorem Thm30:
for Xn being non-empty n-element FinSequence,
X1 being non-empty 1-element FinSequence,
Sn being SemiringFamily of Xn,
S1 be SemiringFamily of X1 st
SemiringProduct(Sn) is semiring_of_sets of product Xn &
SemiringProduct(S1) is semiring_of_sets of product X1 holds
for S12 being Subset-Family of [:product Xn,product X1:] st
S12 = the set of all [:s1,s2:] where
s1 is Element of SemiringProduct(Sn),
s2 is Element of SemiringProduct(S1)
holds
ex I being Function of [: product Xn,product X1 :],product(Xn^X1)
st I is one-to-one & I is onto &
(for x,y be FinSequence st x in product Xn & y in product X1 holds
I.(x,y) = x^y) & I.:S12 = SemiringProduct(Sn^S1)
proof
let Xn be non-empty n-element FinSequence,
X1 be non-empty 1-element FinSequence,
Sn be SemiringFamily of Xn,S1 be SemiringFamily of X1;
assume that
A1: SemiringProduct(Sn) is semiring_of_sets of product Xn and
A2: SemiringProduct(S1) is semiring_of_sets of product X1;
let S12 be Subset-Family of [:product Xn,product X1:] such that
A2b: S12 = the set of all [:s1,s2:] where
s1 is Element of SemiringProduct(Sn),
s2 is Element of SemiringProduct(S1);
reconsider S12 as semiring_of_sets of [:product Xn,product X1:]
by A1,A2,A2b,Thm29;
A3: 1 in Seg 1 & S1 is SemiringFamily of X1 by FINSEQ_1:3;
then
A4: S1.1 is semiring_of_sets of X1.1 by Def2;
A5: S1.1 is non empty by A3,Def2;
A6: 1 in Seg 1 by FINSEQ_1:3;
then
A7: union(S1.1) c= (X1.1) by Thm17;
consider I be Function of [: product Xn,product X1 :],product(Xn^X1)
such that
A8: I is one-to-one and
A9: I is onto and
A10: for x,y be FinSequence st x in product Xn & y in product X1
holds I.(x,y) = x^y by PRVECT_3:6;
take I;
I.:S12 = SemiringProduct(Sn^S1)
proof
hereby
let t be object;
assume t in I.:S12;
then consider s12 be Subset of [:product Xn,product X1:] such that
A12: s12 in S12 and
A13: t = I.:s12 by FUNCT_2:def 10;
consider s1 be Element of SemiringProduct(Sn),
s2 be Element of SemiringProduct(S1) such that
A14: s12 = [:s1,s2:] by A2b,A12;
consider g1 be Function such that
A15: s1 = product g1 and
A16: g1 in product Sn by A1,Def3;
A17: s2 in SemiringProduct(S1) by A2;
s2 in the set of all product <*s*> where s is Element of S1.1
by A17,Thm24;
then consider s11 be Element of S1.1 such that
A18: s2 = product <*s11*>;
reconsider g1 as n-element FinSequence by A16,Thm18;
A19: dom Xn = Seg n & dom Sn = Seg n & dom X1 = Seg 1 &
dom S1 = Seg 1 by FINSEQ_1:89;
A20: dom g1 = Seg n by FINSEQ_1:89;
A21: len g1 = n by FINSEQ_3:153;
A22: dom (g1^<*s11*>) = Seg (n+1) by FINSEQ_1:89;
A23: dom I = [:product Xn,product X1:] by FUNCT_2:def 1;
now
product (g1^<*s11*>) = I.:[:product g1,product <*s11*>:]
proof
hereby
let u be object;
assume u in product(g1^<*s11*>);
then consider v be Function such that
A24: u = v and
A25: dom v = dom (g1^<*s11*>) and
A26: for y being object st y in dom (g1^<*s11*>) holds
v.y in (g1^<*s11*>).y by CARD_3:def 5;
A27: dom v = Seg (n+1) by A25,FINSEQ_1:89;
then
reconsider v as FinSequence by FINSEQ_1:def 2;
card dom v = card Seg (n+1) by A25,FINSEQ_1:89;
then
card dom v = n+1 by FINSEQ_1:57;
then card v = n+1 by CARD_1:62;
then reconsider v as (n+1)-element FinSequence by CARD_1:def 7;
reconsider v1 = v|Seg n as FinSequence by FINSEQ_1:15;
len v = n+1 by FINSEQ_3:153;
then
A28: n <= len v by NAT_1:11;
then
A29: dom v1 = Seg n by FINSEQ_1:17;
set w=[v|Seg n,<*v.(n+1)*>];
A30: now
now
A31: dom (v|Seg n) = Seg n & dom Xn = Seg n
by A29,FINSEQ_1:89;
thus dom(v|Seg n)=dom Xn by A29,FINSEQ_1:89;
let y be object;
assume
A32: y in dom Xn; then
A33: y in Seg n & Seg n c= Seg (n+1) by FINSEQ_1:89,FINSEQ_3:18;
y in dom (v|Seg n) by A32,FINSEQ_1:89,A29; then
A34: (v|Seg n).y = v.y by FUNCT_1:47;
A35: v.y in (g1^<*s11*>).y by A33,A22,A26;
A36: (v|Seg n).y in g1.y
by A34,A35,A32,A20,A31,FINSEQ_1:def 7;
A37: g1 in product Sn & y in dom Sn by A16,A32,Thm16;
consider gg be Function such that
A38: gg = g1 and
dom gg = dom Sn and
A39: for y be object st y in dom Sn holds gg.y in Sn.y
by A16,CARD_3:def 5;
g1.y in Sn.y by A37,A38,A39;
then
A40: (v|Seg n).y in union (Sn.y) & y in Seg n
by A32,FINSEQ_1:89,A36,TARSKI:def 4;
union (Sn.y) c= Xn.y by A33,Thm17;
hence (v|Seg n).y in Xn.y by A40;
end;
hence v|Seg n in product Xn by CARD_3:def 5;
A41: v.(n+1) in (g1^<*s11*>).(n+1) by A22,FINSEQ_1:4,A26;
(g1^<*s11*>).(n + 1) = s11 by A21,FINSEQ_1:42;
then v.(n+1) in union (S1.1) & union (S1.1) c= X1.1
by A41,A5,A6,Thm17,TARSKI:def 4;
then <*v.(n+1)*> in the set of all <*a*> where
a is Element of X1.1;
hence <*v.(n+1)*> in product X1 by Thm21;
end;
now
thus w in dom I by ZFMISC_1:def 2,A30,A23;
now
now
thus dom v1 = dom g1 by A28,FINSEQ_1:17,A20;
now
let y be object;
assume
A42: y in dom g1; then
A43: y in Seg n & Seg n c= Seg (n+1)
by FINSEQ_1:89,FINSEQ_3:18;
A44: (v|Seg n).y = v.y by A42,A20,A29,FUNCT_1:47;
v.y in (g1^<*s11*>).y by A43,A22,A26;
hence v1.y in g1.y by A44,A42,FINSEQ_1:def 7;
end;
hence for y being object st y in dom g1 holds v1.y in g1.y;
end;
hence v|Seg n in product g1 by CARD_3:def 5;
A46: v.(n+1) in (g1^<*s11*>).(n+1) by A22,A26,FINSEQ_1:4;
now
dom <*v.(n+1)*> = Seg 1 &
dom <*s11*> = Seg 1 by FINSEQ_1:def 8;
hence dom <*v.(n+1)*> = dom <*s11*>;
let y be object;
assume y in dom <*s11*>;
then y in Seg 1 & Seg 1 = {1}
by FINSEQ_1:def 8,FINSEQ_1:2; then
A47: y = 1 by TARSKI:def 1;
thus <*v.(n+1)*>.y in <*s11*>.y
by A21,A46,FINSEQ_1:42,A47;
end;
hence <*v.(n+1)*> in product <*s11*> by CARD_3:def 5;
end;
hence w in [:product g1,product <*s11*>:]
by ZFMISC_1:def 2;
A48: I.w = I.(v1,<*v.(n+1)*>) by BINOP_1:def 1;
v1 ^ <*v.(n+1)*> = v|Seg (n+1) by A27,FINSEQ_1:4,FINSEQ_5:10;
hence u = I.w by A48,A30,A10,A24,A27;
end;
hence u in I.:[:product g1,product <*s11*>:] by FUNCT_1:def 6;
end;
let u be object;
assume
u in I.:[:product g1,product <*s11*>:];
then consider v be object such that
v in dom I and
A50: v in [:product g1,product <*s11*>:] and
A51: u = I.v by FUNCT_1:def 6;
consider va,vb be object such that
A52: va in product g1 and
A53: vb in product <*s11*> and
A54: v=[va,vb] by A50,ZFMISC_1:def 2;
consider wa be Function such that
A55: wa=va and
A56: dom wa = dom g1 and
A57: for y be object st y in dom g1 holds
wa.y in g1.y by A52,CARD_3:def 5;
consider wb be Function such that
A58: wb=vb and
A59: dom wb = dom <*s11*> and
A60: for y be object st y in dom <*s11*> holds wb.y in <*s11*>.y
by A53,CARD_3:def 5;
A61: dom g1 = Seg n by FINSEQ_1:89;
then reconsider wa as FinSequence by A56,FINSEQ_1:def 2;
reconsider wa as n-element FinSequence by A55,A52,Thm18;
reconsider wb as FinSequence by A59,FINSEQ_1:def 8,FINSEQ_1:def 2;
card dom wb = 1 by A59,CARD_1:def 7;
then card wb = 1 by CARD_1:62;
then reconsider wb as 1-element FinSequence by CARD_1:def 7;
reconsider w=wa^wb as (n+1)-element FinSequence;
now
A62: now
now
thus dom wa = dom Xn by FINSEQ_1:89,A19;
let y be object;
assume
A63: y in dom Xn;
then y in dom g1 by FINSEQ_1:89,A19;
then
A64: wa.y in g1.y by A57;
consider gg1 be Function such that
A65: gg1=g1 and
dom gg1=dom Sn and
A66: for y be object st y in dom Sn holds gg1.y in Sn.y
by A16,CARD_3:def 5;
g1.y in Sn.y by A63,A19,A65,A66;
then
A67: wa.y in union(Sn.y) by A64,TARSKI:def 4;
union (Sn.y) c= Xn.y by A63,A19,Thm17;
hence wa.y in Xn.y by A67;
end;
hence wa in product Xn by CARD_3:def 5;
now
thus dom wb = dom X1 by FINSEQ_1:89,A19;
let y be object;
assume
A68: y in dom X1;
y in dom <*s11*> by A68,A19,FINSEQ_1:def 8;
then
A69: wb.y in <*s11*>.y by A60;
A70: y = 1 by A68,A19,FINSEQ_1:2,TARSKI:def 1;
then
A71: wb.y in s11 by A69;
wb.y in union (S1.1) by A71,A5,TARSKI:def 4;
hence wb.y in X1.y by A70,A7;
end;
hence wb in product X1 by CARD_3:def 5;
end;
I.[va,vb]= I.(wa,wb) by A55,A58,BINOP_1:def 1;
hence u = w by A54,A51,A10,A62;
A73: dom (g1^<*s11*>) = Seg (n+1) & dom w = Seg (n+1) by FINSEQ_1:89;
hence dom w = dom (g1^<*s11*>);
hereby
let y be object;
assume y in dom (g1^<*s11*>);
then y in Seg n \/ {n+1} by A73,FINSEQ_1:9;
then y in Seg n or y in {n+1} by XBOOLE_0:def 3;
then per cases by TARSKI:def 1;
suppose
A74: y in Seg n;
then
A75: y in dom g1 by FINSEQ_1:89;
(g1^<*s11*>).y = g1.y & wa.y in g1.y
by A74,A61,A57,FINSEQ_1:def 7;
hence w.y in (g1^<*s11*>).y by A56,FINSEQ_1:def 7,A75;
end;
suppose
A77: y = n+1;
then
A78: (g1^<*s11*>).y = s11 by A21,FINSEQ_1:42;
dom wb = dom X1 by FINSEQ_1:89,A19;
then 1 in dom wb by A19,FINSEQ_1:2,TARSKI:def 1;
then
A79: wb.1 = w.(len wa+1) by FINSEQ_1:def 7;
A80: len wa + 1 = n + 1 by FINSEQ_3:153;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*s11*> by FINSEQ_1:def 8;
then w.y in <*s11*>.1 by A60,A80,A77,A79;
hence w.y in (g1^<*s11*>).y by A78;
end;
end;
end;
hence u in product (g1^<*s11*>) by CARD_3:def 5;
end;
hence t = product (g1^<*s11*>) by A13,A14,A15,A18;
now
A81: len (Sn^S1) = n + 1 by FINSEQ_3:153;
then
A82: dom (Sn^S1) = Seg (n+1) by FINSEQ_1:def 3;
thus dom (g1^<*s11*>) = dom (Sn^S1) by A81,A22,FINSEQ_1:def 3;
let u be object;
assume u in dom (Sn^S1);
then u in Seg n \/ {n+1} by A82,FINSEQ_1:9;
then u in Seg n or u in {n+1} by XBOOLE_0:def 3;
then per cases by TARSKI:def 1;
suppose
A83: u in Seg n; then
A84: u in dom Sn by FINSEQ_1:89;
A85: (Sn^S1).u = Sn.u by A19,A83,FINSEQ_1:def 7;
dom g1 = Seg n by FINSEQ_1:89;
then
A86: (g1^<*s11*>).u = g1.u by A83,FINSEQ_1:def 7;
consider gg1 be Function such that
A87: g1=gg1 and
dom gg1 = dom Sn and
A88: for y be object st y in dom Sn holds gg1.y in Sn.y
by A16,CARD_3:def 5;
thus (g1^<*s11*>).u in (Sn^S1).u by A87,A88,A84,A86,A85;
end;
suppose
A89: u = n+1;
then
A90: (g1^<*s11*>).u = s11 by A21,FINSEQ_1:42;
A91: s11 in S1.1 by A5;
1 in dom S1 & len Sn = n by A19,FINSEQ_1:3,FINSEQ_3:153;
hence (g1^<*s11*>).u in (Sn^S1).u
by A89,A90,A91,FINSEQ_1:def 7;
end;
end;
hence g1^<*s11*> in product(Sn^S1) by CARD_3:def 5;
end;
hence t in SemiringProduct(Sn^S1) by Def3;
end;
let t be object;
assume t in SemiringProduct(Sn^S1);
then consider f being Function such that
A92: t = product f and
A93: f in product (Sn^S1) by Def3;
consider g be Function such that
A94: f=g and
A95: dom g = dom (Sn^S1) and
A96: for y be object st y in dom (Sn^S1) holds g.y in (Sn^S1).y
by A93,CARD_3:def 5;
A97: dom Xn = Seg n & dom Sn = Seg n & dom X1 = Seg 1 &
dom S1 = Seg 1 by FINSEQ_1:89;
dom X1 = {1} & dom S1={1} by FINSEQ_1:2,FINSEQ_1:89;
then
A98: 1 in dom X1 & 1 in dom S1 by TARSKI:def 1;
A99: len Xn = n & len Sn = n & len X1 = 1 & len S1 = 1 by FINSEQ_3:153;
A100: len(Sn^S1) = n + 1 by FINSEQ_3:153;
then
A101: dom (Sn^S1) = Seg (n+1) by FINSEQ_1:def 3;
dom g = Seg(n+1) by A95,A100,FINSEQ_1:def 3;
then reconsider g as FinSequence by FINSEQ_1:def 2;
card dom g = n+1 by A95,CARD_1:def 7;
then card g = n+1 by CARD_1:62;
then reconsider g as (n+1)-element FinSequence by CARD_1:def 7;
reconsider t0=t as set by TARSKI:1;
now
let a be object;
assume
a in product f;
then consider b be Function such that
A102: a=b and
A103: dom b = dom f and
A104: for y be object st y in dom f holds b.y in f.y by CARD_3:def 5;
now
take b;
thus a=b by A102;
len (Sn^S1) = n + 1 by FINSEQ_3:153;
then
A105: dom (Sn^S1) = Seg (n+1) by FINSEQ_1:def 3;
A106: dom f = Seg (n+1) by A105,A93,CARD_3:9;
A107: dom b = Seg (n+1) by A103,A105,A93,CARD_3:9;
A108: len (Xn^X1) = n + 1 by FINSEQ_3:153;
then
A109: dom (Xn^X1) = Seg (n+1) by FINSEQ_1:def 3;
thus dom b = dom (Xn^X1) by A108,A107,FINSEQ_1:def 3;
let y be object;
assume
A110: y in dom(Xn^X1);
then
A111: b.y in f.y by A104,A106,A109;
g.y in (Sn^S1).y by A96,A105,A109,A110;
then
A112: b.y in union ((Sn^S1).y) by A111,A94,TARSKI:def 4;
y in Seg n \/ {n+1} by A110,A109,FINSEQ_1:9;
then y in Seg n or y in {n+1} by XBOOLE_0:def 3;
then per cases by TARSKI:def 1;
suppose
A113: y in Seg n; then
A114: (Xn^X1).y = Xn.y by A97,FINSEQ_1:def 7;
Sn.y is semiring_of_sets of Xn.y by A113,Def2;
then union (Sn.y) c= union bool (Xn.y) by ZFMISC_1:77;
then
union (Sn.y) c= Xn.y &
union ((Sn^S1).y) = union(Sn.y)
by ZFMISC_1:81,A97,A113,FINSEQ_1:def 7;
hence b.y in (Xn^X1).y by A112,A114;
end;
suppose
A116: y = n+1; then
A117: (Xn^X1).y = X1.1 by A99,A98,FINSEQ_1:def 7;
union (S1.1) c= union bool (X1.1) by A4,ZFMISC_1:77;
then
union (S1.1) c= X1.1 & union ((Sn^S1).y) =
union (S1.1) by A116,A99,A98,FINSEQ_1:def 7,ZFMISC_1:81;
hence b.y in (Xn^X1).y by A112,A117;
end;
end;
hence a in product(Xn^X1) by CARD_3:def 5;
end;
then t0 c= product(Xn^X1) by A92;
then reconsider t1=t0 as Subset of product(Xn^X1);
reconsider hn=product (g|n) as set;
n <= n+1 & len g = n+1 by NAT_1:11,FINSEQ_3:153;
then
A118b:len (g|n)=n by FINSEQ_1:59;
then
A119: dom (g|n) = Seg n by FINSEQ_1:def 3;
A120: now
let a be object;
assume a in hn;
then consider b be Function such that
A121: a=b and
A122: dom b = dom (g|n) and
A123: for y be object st y in dom (g|n) holds b.y in (g|n).y
by CARD_3:def 5;
now
thus dom b = dom Xn by A122,A118b,FINSEQ_1:def 3,A97;
let y be object;
assume
A124: y in dom Xn;
then
A125: y in Seg n by FINSEQ_1:89;
b.y in (g|n).y by A124,A97,A119,A123;
then b.y in (g|Seg n).y by FINSEQ_1:def 16;
then
A126: b.y in g.y by A125,FUNCT_1:49;
Seg n c= Seg (n+1) by NAT_1:11,FINSEQ_1:5;
then
A127: g.y in (Sn^S1).y by A101,A96,A125;
g.y in Sn.y by A124,A127,A97,FINSEQ_1:def 7;
then
A128: b.y in union (Sn.y) by A126,TARSKI:def 4;
Sn.y is semiring_of_sets of Xn.y by A125,Def2;
then union (Sn.y) c= union bool (Xn.y) by ZFMISC_1:77;
then union(Sn.y) c= Xn.y by ZFMISC_1:81;
hence b.y in Xn.y by A128;
end;
hence a in product Xn by A121,CARD_3:def 5;
end;
then
A129: hn c= product Xn;
reconsider h1=product <*g.(n+1)*> as set;
A130: now
let a be object;
assume a in h1;
then consider b be Function such that
A131: a=b and
A132: dom b = dom <*g.(n+1)*> and
A133: for y be object st y in dom <*g.(n+1)*> holds b.y in <*g.(n+1)*>.y
by CARD_3:def 5;
A134: dom <*g.(n+1)*> = Seg 1 by FINSEQ_1:def 8;
now
thus dom b = dom X1 by A132,FINSEQ_1:def 8,A97;
let y be object;
assume
A135: y in dom X1;
then
A136: y in Seg 1 by FINSEQ_1:89;
A137: b.y in <*g.(n+1)*>.y by A135,A133,A134,A97;
A138: y=1 by A136,FINSEQ_1:2,TARSKI:def 1;
1 in dom S1 & len Sn = n by A97,FINSEQ_1:3,FINSEQ_3:153;
then (Sn^S1).(len Sn + 1) = S1.1 & dom (Sn^S1) = Seg (n+1)
by A99,FINSEQ_1:def 7;
then b.y in g.(n+1) & g.(n+1) in S1.1
by A138,A137,A96,A99,FINSEQ_1:3;
then
A139: b.y in union (S1.1) by TARSKI:def 4;
union (S1.1) c= union bool (X1.1) by A4,ZFMISC_1:77;
then union(S1.1) c= X1.1 by ZFMISC_1:81;
hence b.y in X1.y by A139,A138;
end;
hence a in product X1 by A131,CARD_3:def 5;
end;
then h1 c= product X1;
then reconsider s12=[:hn,h1:] as Subset of [:product Xn,product X1:]
by A129,ZFMISC_1:96;
now
now
now
thus hn = product (g|n);
now
thus dom (g|n) = dom Sn by A119,FINSEQ_1:89;
let y be object;
assume
A140: y in dom Sn;
then
A141: y in Seg n by FINSEQ_1:89;
Seg n c= Seg (n+1) by NAT_1:11,FINSEQ_1:5;
then
A142: g.y in (Sn^S1).y by A96,A101,A141;
A143: g.y in Sn.y by A142,A140,FINSEQ_1:def 7;
y in dom (g|Seg n) by A141,A119,FINSEQ_1:def 16;
then g.y = (g|Seg n).y by FUNCT_1:47;
hence (g|n).y in Sn.y by A143,FINSEQ_1:def 16;
end;
hence g|n in product(Sn) by CARD_3:def 5;
end;
hence hn is Element of SemiringProduct(Sn) by Def3;
now
thus h1 = product <*g.(n+1)*>;
now
thus dom <*g.(n+1)*> = dom S1 by FINSEQ_1:def 8,A97;
let b be object;
assume b in dom S1;
then
A144: b = 1 by A97,FINSEQ_1:2,TARSKI:def 1;
<*g.(n+1)*>.1 in (Sn^S1).(n+1) & 1 in dom S1
by A96,FINSEQ_1:4,A101,A97,FINSEQ_1:2,TARSKI:def 1;
hence <*g.(n+1)*>.b in S1.b by A144,A99,FINSEQ_1:def 7;
end;
hence <*g.(n+1)*> in product S1 by CARD_3:def 5;
end;
hence h1 is Element of SemiringProduct(S1) by Def3;
end;
hence s12 in S12 by A2b;
now
hereby
let u be object;
assume u in I.:[:hn,h1:];
then consider v be object such that
v in dom I and
A146: v in [:hn,h1:] and
A147: u = I.v by FUNCT_1:def 6;
consider va,vb be object such that
A148: va in hn and
A149: vb in h1 and
A150: v = [va,vb] by A146,ZFMISC_1:def 2;
A151: va in product Xn & vb in product X1 by A120,A130,A148,A149;
reconsider va as n-element FinSequence by A120,A148,Thm18;
reconsider vb as 1-element FinSequence by A149,Thm18;
A152: u = I.(va,vb) by A147,A150,BINOP_1:def 1
.=va^vb by A10,A151;
set vab=va^vb;
len (Sn^S1) = n + 1 by FINSEQ_3:153;
then
A153: dom (Sn^S1) = Seg (n+1) by FINSEQ_1:def 3;
then
A154: dom f = Seg (n+1) by A93,CARD_3:9;
A155: dom (va^vb) = Seg (n+1) by FINSEQ_1:89;
now
thus dom vab = dom f by A153,A93,CARD_3:9,A155;
let y be object;
assume y in dom f;
then y in Seg n \/ {n+1} by A154,FINSEQ_1:9;
then y in Seg n or y in {n+1} by XBOOLE_0:def 3;
then per cases by TARSKI:def 1;
suppose
A156: y in Seg n; then
A157: y in dom va by FINSEQ_1:89;
then
A158: vab.y = va.y by FINSEQ_1:def 7;
consider va1 be Function such that
A159: va1=va and
A160: dom va1 = dom (g|n) and
A161: for y be object st y in dom (g|n) holds
va1.y in (g|n).y by A148,CARD_3:def 5;
va1.y in (g|n).y by A157,A159,A160,A161;
then va1.y in (g|Seg n).y by FINSEQ_1:def 16;
hence vab.y in f.y by A94,A156,A158,A159,FUNCT_1:49;
end;
suppose
A162: y = n+1;
now
dom vb = Seg 1 by FINSEQ_1:89;
hence 1 in dom vb by FINSEQ_1:2,TARSKI:def 1;
thus y = len va +1 by A162,FINSEQ_3:153;
end;
then
A163: (va^vb).y = vb.1 by FINSEQ_1:def 7;
consider vb1 be Function such that
A164: vb=vb1 and
dom vb1 = dom <*g.(n+1)*> and
A165: for y be object st y in dom <*g.(n+1)*> holds
vb1.y in <*g.(n+1)*>.y by A149,CARD_3:def 5;
dom (<*g.(n+1)*>) = Seg 1 by FINSEQ_1:def 8;
then 1 in dom (<*g.(n+1)*>) by FINSEQ_1:2,TARSKI:def 1;
then vb1.1 in <*g.(n+1)*>.1 by A165;
hence vab.y in f.y by A164,A163,A162,A94;
end;
end;
hence u in product f by A152,CARD_3:def 5;
end;
let u be object;
assume u in product f;
then consider v be Function such that
A166: u=v and
A167: dom v = dom f and
A168: for y be object st y in dom f holds v.y in f.y by CARD_3:def 5;
len (Sn^S1) = n + 1 by FINSEQ_3:153;
then
A169: dom (Sn^S1) = Seg (n+1) by FINSEQ_1:def 3;
A170: dom f = Seg (n+1) by A93,A169,CARD_3:9;
A171: dom v = Seg (n+1) by A93,A167,A169,CARD_3:9;
reconsider v as FinSequence by A93,A167,A169,CARD_3:9,FINSEQ_1:def 2;
card dom v = n+1 by A171,FINSEQ_1:57;
then card v = n+1 by CARD_1:62;
then reconsider v as (n+1)-element FinSequence by CARD_1:def 7;
reconsider xn=v|Seg n as FinSequence by FINSEQ_1:15;
reconsider x1=<*v.(n+1)*> as 1-element FinSequence;
A172: xn in product Xn & x1 in product X1
proof
now
len v = n+1 by FINSEQ_3:153;
then
A173: n <= len v by NAT_1:11;
then
A174: dom xn = Seg n by FINSEQ_1:17;
thus dom xn = dom Xn by A173,FINSEQ_1:17,A97;
let y be object;
assume
A175: y in dom Xn;
A176: y in Seg n & Seg n c= Seg (n+1)
by NAT_1:11,A175,FINSEQ_1:89,FINSEQ_1:5;
A177: v.y in f.y by A176,A170,A168;
A178: f.y in (Sn^S1).y by A176,A101,A94,A96;
A179: f.y in Sn.y by A175,A97,A178,FINSEQ_1:def 7;
Sn.y is semiring_of_sets of Xn.y by A175,A97,Def2;
then union (Sn.y) c= union bool (Xn.y) by ZFMISC_1:77;
then
A180: union(Sn.y) c= Xn.y by ZFMISC_1:81;
v.y in union (Sn.y) by A179,A177,TARSKI:def 4;
then v.y in Xn.y by A180;
hence xn.y in Xn.y by A174,A175,A97,FUNCT_1:47;
end;
hence xn in product Xn by CARD_3:def 5;
now
thus dom x1 = dom X1 by A97,FINSEQ_1:def 8;
let y be object;
assume y in dom X1;
then
A181: y = 1 by A97,FINSEQ_1:2,TARSKI:def 1;
1 in dom S1 & len Sn = n by A97,FINSEQ_1:3,FINSEQ_3:153;
then (Sn^S1).(len Sn + 1) = S1.1 & dom (Sn^S1) = Seg (n+1)
by A99,FINSEQ_1:def 7;
then v.(n+1) in f.(n+1) & f.(n+1) in S1.1
by A99,A94,A96,A170,A168,FINSEQ_1:4;
then v.(n+1) in union (S1.1) & union (S1.1) c= X1.1
by A6,Thm17,TARSKI:def 4;
hence x1.y in X1.y by A181;
end;
hence x1 in product X1 by CARD_3:def 5;
end;
set x=[xn,x1];
now
dom I = [:product Xn,product X1:] by FUNCT_2:def 1;
hence [xn,x1] in dom I by A172,ZFMISC_1:def 2;
now
now
len v = n+1 by FINSEQ_3:153;
then n <= len v by NAT_1:11;
then
A183: dom xn = Seg n by FINSEQ_1:17;
then
A184: dom (v|Seg n) = Seg n & Seg n = dom (g|n)
by A118b,FINSEQ_1:def 3;
thus
A185: dom (v|Seg n) = dom (g|n) by A183,A118b,FINSEQ_1:def 3;
let y be object;
assume
A186: y in dom (g|n);
then
A187: v|(Seg n).y = v.y by A185,FUNCT_1:47;
Seg n c= Seg (n+1) & dom (g|n) = Seg n & dom f = Seg(n+1)
by NAT_1:11,A118b,FINSEQ_1:def 3,A93,A169,CARD_3:9,
FINSEQ_1:5;
then
A188: v.y in g.y by A94,A168,A186;
(g|Seg n).y=g.y by A186,A184,FUNCT_1:49;
hence (v|Seg n).y in (g|n).y by A187,A188,FINSEQ_1:def 16;
end;
hence xn in hn by CARD_3:def 5;
now
dom x1 = dom X1 by A97,FINSEQ_1:def 8;
hence dom x1 = dom <*g.(n+1)*> by A97,FINSEQ_1:def 8;
let y be object;
assume y in dom <*g.(n+1)*>;
then y in Seg 1 by FINSEQ_1:def 8;
then
A189: y = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A190: <*g.(n+1)*>.y = g.(n+1);
x1.y = v.(n+1) by A189;
hence x1.y in <*g.(n+1)*>.y
by A168,A170,FINSEQ_1:4,A94,A190;
end;
hence x1 in h1 by CARD_3:def 5;
thus x=[xn,x1];
end;
hence x in [:hn,h1:] by ZFMISC_1:def 2;
now
A191: I.x = I.(xn,x1) by BINOP_1:def 1
.= xn^x1 by A10,A172;
xn ^ <*v.(n+1)*> = v|Seg (n+1) by A171,FINSEQ_1:4,FINSEQ_5:10;
hence I.x = v by A171,A191;
end;
hence u=I.x by A166;
end;
hence u in I.:[:hn,h1:] by FUNCT_1:def 6;
end;
then I.:[:hn,h1:] c= product f & product f c= I.:[:hn,h1:];
hence t1 = I.:s12 by A92;
end;
hence thesis by FUNCT_2:def 10;
end;
hence thesis by A8,A9,A10;
end;
theorem Thm31:
for Xn being non-empty n-element FinSequence,
X1 being non-empty 1-element FinSequence,
Sn being SemiringFamily of Xn, S1 be SemiringFamily of X1 st
SemiringProduct(Sn) is semiring_of_sets of product Xn &
SemiringProduct(S1) is semiring_of_sets of product X1 holds
SemiringProduct(Sn^S1) is semiring_of_sets of product (Xn^X1)
proof
let Xn be non-empty n-element FinSequence,
X1 be non-empty 1-element FinSequence, Sn be SemiringFamily of Xn,
S1 be SemiringFamily of X1;
assume that
A1: SemiringProduct(Sn) is semiring_of_sets of product Xn and
A2: SemiringProduct(S1) is semiring_of_sets of product X1;
reconsider S12 = the set of all [:s1,s2:] where
s1 is Element of SemiringProduct(Sn),
s2 is Element of SemiringProduct(S1) as
semiring_of_sets of [:product Xn,product X1:] by A1,A2,Thm29;
consider I be Function of [: product Xn,product X1 :],product(Xn^X1)
such that
A3: I is one-to-one and
I is onto and
for x,y be FinSequence st x in product Xn & y in product X1
holds I.(x,y) = x^y and
A4: I.:S12 = SemiringProduct(Sn^S1) by A1,A2,Thm30;
thus thesis by A3,A4,Thm11,Thm12;
end;
:: Product of n semiring of sets is semiring of sets
theorem Thm32:
for S being SemiringFamily of X holds
SemiringProduct(S) is semiring_of_sets of product X
proof
let S being SemiringFamily of X;
reconsider SP=SemiringProduct(S) as Subset-Family of product X by Thm20;
defpred P[non zero Nat] means
for X be non-empty $1-element FinSequence, S be SemiringFamily of X holds
SemiringProduct(S) is semiring_of_sets of product X;
A1: P[1] by Thm28;
A2: now
let n be non zero Nat;
assume
A3: P[n];
now
let X be non-empty (n+1)-element FinSequence,
S be SemiringFamily of X;
reconsider SPS = SemiringProduct(S) as Subset-Family of product X
by Thm20;
consider Xq be FinSequence,xq be object such that
A4: X = Xq ^ <*xq*> by FINSEQ_1:46;
len X = len Xq + len <*xq*> by A4,FINSEQ_1:22
.= len Xq + 1 by FINSEQ_1:39; then
A5: len Xq = n by XCMPLX_1:2,FINSEQ_3:153;
reconsider Xn=Xq as n-element FinSequence by A5,CARD_1:def 7;
rng Xn c= rng X by A4,FINSEQ_1:29; then
A7: not {} in rng Xn;
reconsider Xn as non-empty n-element FinSequence by A7,RELAT_1:def 9;
reconsider X1=<*xq*> as 1-element FinSequence;
rng X1 c= rng X by A4,FINSEQ_1:30; then
A9: not {} in rng X1;
reconsider X1 as non-empty 1-element FinSequence by A9,RELAT_1:def 9;
consider Sq be FinSequence, sq be object such that
A10: S = Sq ^ <*sq*> by FINSEQ_1:46;
len S = len Sq + len <*sq*> by A10,FINSEQ_1:22
.= len Sq + 1 by FINSEQ_1:39;
then len Sq = n by FINSEQ_3:153,XCMPLX_1:2;
then reconsider Sn=Sq as n-element FinSequence by CARD_1:def 7;
reconsider S1=<*sq*> as 1-element FinSequence;
Seg (n+1) = Seg n \/ {n+1} by FINSEQ_1:9;
then
A11: Seg n c= Seg (n+1) by XBOOLE_1:7;
A12: len Xn = n & len Sn = n by FINSEQ_3:153;
now
now
let i be Nat;
assume
A14: i in Seg n;
then i in Seg len Xn & i in Seg len Sn by FINSEQ_3:153;
then X.i = (Xn ^ X1).i & S.i= (Sn ^ S1).i & 1 <= i & i <= len Xn &
i <= len Sn by A4,A10,FINSEQ_1:1;
then X.i = Xn.i & S.i = Sn.i by FINSEQ_1:64;
hence Sn.i is semiring_of_sets of Xn.i by A14,A11,Def2;
end;
hence Sn is SemiringFamily of Xn by Def2;
end;
then
A16: Xn is non-empty & Sn is SemiringFamily of Xn & SemiringProduct(Sn) is
semiring_of_sets of product Xn by A3;
A17: len X1 = 1 by FINSEQ_1:39;
then
A18: X1.1 = X.(n+1) by FINSEQ_1:65,A4,A12;
len S1 = 1 by FINSEQ_1:39;
then
A20: S1.1 = S.(n+1) by FINSEQ_1:65,A12,A10;
now
thus X1 is non-empty;
A23: n+1 in Seg (n+1) by FINSEQ_1:3;
now
let i be Nat;
assume i in Seg 1;
then i=1 by TARSKI:def 1,FINSEQ_1:2;
hence S1.i is semiring_of_sets of X1.i
by A23,A20,A18,Def2;
end;
hence X1.1=X.(n+1) & S1 is SemiringFamily of X1
by A4,A12,A17,FINSEQ_1:65,Def2;
end; then
S1 is SemiringFamily of X1 &
SemiringProduct(S1) is semiring_of_sets of product X1 by Thm28;
hence SemiringProduct(S) is semiring_of_sets of product X
by A16,Thm31,A4,A10;
end;
hence P[n + 1];
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
definition
let n be non zero Nat,
X be non-empty n-element FinSequence,
S be SemiringFamily of X;
attr S is cap-closed-yielding means :Def4:
for i being Nat st i in Seg n holds S.i is cap-closed;
end;
registration
let n be non zero Nat, X be non-empty n-element FinSequence;
cluster cap-closed-yielding for SemiringFamily of X;
existence
proof
deffunc F(set)=bool (X.$1);
consider p being FinSequence such that
A1: len p = n and
A2: for i being Nat st i in dom p holds p.i=F(i)
from FINSEQ_1:sch 2;
reconsider p as n-element FinSequence by A1,CARD_1:def 7;
take p;
now
let i be Nat;
assume
A3: i in Seg n;
reconsider Xi=X.i as set;
A4: bool Xi is semiring_of_sets of Xi by SRINGS_2:5;
i in dom p by A3,A1,FINSEQ_1:def 3;
hence p.i is semiring_of_sets of X.i by A2,A4;
end;
then reconsider p as SemiringFamily of X by Def2;
now
let i be Nat;
assume i in Seg n;
then i in dom p by A1,FINSEQ_1:def 3;
then p.i = bool (X.i) by A2;
hence p.i is cap-closed;
end;
then p is cap-closed-yielding;
hence thesis;
end;
end;
begin :: Finite Product of Classical Semiring of Sets
registration
let X being set;
cluster cap-closed for semiring_of_sets of X;
existence
proof
reconsider S = bool X as semiring_of_sets of X by SRINGS_2:5;
S is cap-closed;
hence thesis;
end;
end;
theorem Thm33:
for X being non-empty 1-element FinSequence,
S being cap-closed-yielding SemiringFamily of X holds
the set of all product <*s*> where s is Element of S.1 is
cap-closed semiring_of_sets of the set of all <*x*> where x is Element of X.1
proof
let X be non-empty 1-element FinSequence,
S be cap-closed-yielding SemiringFamily of X;
S is cap-closed-yielding SemiringFamily of X & 1 in Seg 1 by FINSEQ_1:3;
then
A1: S.1 is semiring_of_sets of X.1 & S.1 is cap-closed by Def2,Def4;
set S1=the set of all product <*s*> where s is Element of S.1;
set X1=the set of all <*x*> where x is Element of X.1;
now
let s1,s2 be set;
assume that
A2: s1 in S1 and
A3: s2 in S1;
consider t1 be Element of S.1 such that
A4: s1 = product <*t1*> by A2;
consider t2 be Element of S.1 such that
A5: s2 = product <*t2*> by A3;
A6: s1/\s2 = product <*t1/\t2*> by A4,A5,Thm25;
t1/\t2 is Element of S.1 by A1;
hence s1/\s2 in S1 by A6;
end;
then S1 is cap-closed;
hence thesis by Thm27;
end;
theorem Thm34:
for X being non-empty 1-element FinSequence,
S being cap-closed-yielding SemiringFamily of X
holds SemiringProduct(S) is cap-closed semiring_of_sets of product X
proof
let X being non-empty 1-element FinSequence,
S being cap-closed-yielding SemiringFamily of X;
set S1=the set of all product <*s*> where s is Element of S.1;
set X1=the set of all <*x*> where x is Element of X.1;
S1 = SemiringProduct(S) & X1 = product X by Thm21,Thm24;
hence thesis by Thm33;
end;
theorem Thm35:
for X1,X2 being set, S1 being cap-closed semiring_of_sets of X1,
S2 being cap-closed semiring_of_sets of X2 holds
the set of all [:s1,s2:] where s1 is Element of S1,
s2 is Element of S2 is cap-closed semiring_of_sets of [:X1,X2:]
proof
let X1,X2 be set, S1 be cap-closed semiring_of_sets of X1,
S2 be cap-closed semiring_of_sets of X2;
set S = {s where s is Subset of [:X1,X2:]:ex x1,x2 be set st x1 in S1 &
x2 in S2 & s=[:x1,x2:]};
S is semiring_of_sets of [:X1,X2:] & S is cap-closed
by SRINGS_2:7,SRINGS_2:3;
hence thesis by SRINGS_2:2;
end;
theorem Thm36:
for Xn being non-empty n-element FinSequence,
X1 being non-empty 1-element FinSequence,
Sn being cap-closed-yielding SemiringFamily of Xn,
S1 be cap-closed-yielding SemiringFamily of X1 st
SemiringProduct(Sn) is cap-closed semiring_of_sets of product Xn &
SemiringProduct(S1) is cap-closed semiring_of_sets of product X1 holds
SemiringProduct(Sn^S1) is cap-closed semiring_of_sets of product (Xn^X1)
proof
let Xn be non-empty n-element FinSequence,
X1 be non-empty 1-element FinSequence,
Sn be cap-closed-yielding SemiringFamily of Xn,
S1 be cap-closed-yielding SemiringFamily of X1;
assume that
A1: SemiringProduct(Sn) is cap-closed semiring_of_sets of product Xn and
A2: SemiringProduct(S1) is cap-closed semiring_of_sets of product X1;
reconsider S12 = the set of all [:s1,s2:] where
s1 is Element of SemiringProduct(Sn),
s2 is Element of SemiringProduct(S1) as
semiring_of_sets of [:product Xn,product X1:] by A1,A2,Thm29;
consider I be Function of [: product Xn,product X1 :],product(Xn^X1)
such that
A3: I is one-to-one and
I is onto and
for x,y be FinSequence st x in product Xn & y in product X1
holds I.(x,y) = x^y and
A4: I.:S12 = SemiringProduct(Sn^S1) by A1,A2,Thm30;
S12 is cap-closed by A1,A2,Thm35;
hence thesis by A3,Thm10,A4,Thm12;
end;
:: Product of n classical semiring of sets is cap-closed
Thm37:
for S being cap-closed-yielding SemiringFamily of X holds
SemiringProduct(S) is cap-closed
proof
let S be cap-closed-yielding SemiringFamily of X;
reconsider SP=SemiringProduct(S) as Subset-Family of product X by Thm20;
defpred P[non zero Nat] means
for X be non-empty $1-element FinSequence,
S be cap-closed-yielding SemiringFamily of X holds
SemiringProduct(S) is cap-closed semiring_of_sets of product X;
A1: P[1] by Thm34;
A2: now
let n be non zero Nat;
assume
A3: P[n];
now
let X be non-empty (n+1)-element FinSequence,
S be cap-closed-yielding SemiringFamily of X;
reconsider SPS = SemiringProduct(S) as Subset-Family of product X
by Thm20;
consider Xq be FinSequence,xq be object such that
A4: X = Xq ^ <*xq*> by FINSEQ_1:46;
len X = len Xq + len <*xq*> by A4,FINSEQ_1:22
.= len Xq + 1 by FINSEQ_1:39; then
A5: len Xq = n by XCMPLX_1:2,FINSEQ_3:153;
reconsider Xn=Xq as n-element FinSequence by A5,CARD_1:def 7;
rng Xn c= rng X by A4,FINSEQ_1:29; then
A7: not {} in rng Xn;
reconsider Xn as non-empty n-element FinSequence by A7,RELAT_1:def 9;
reconsider X1=<*xq*> as 1-element FinSequence;
rng X1 c= rng X by A4,FINSEQ_1:30; then
A9: not {} in rng X1;
reconsider X1 as non-empty 1-element FinSequence by A9,RELAT_1:def 9;
consider Sq be FinSequence, sq be object such that
A10: S = Sq ^ <*sq*> by FINSEQ_1:46;
len S = len Sq + len <*sq*> by A10,FINSEQ_1:22
.= len Sq + 1 by FINSEQ_1:39;
then len Sq = n by FINSEQ_3:153,XCMPLX_1:2;
then reconsider Sn=Sq as n-element FinSequence by CARD_1:def 7;
reconsider S1=<*sq*> as 1-element FinSequence;
Seg (n+1) = Seg n \/ {n+1} by FINSEQ_1:9; then
A11: Seg n c= Seg (n+1) by XBOOLE_1:7;
A12: len Xn = n & len Sn = n by FINSEQ_3:153;
now
A13: for i be Nat st i in Seg n holds
Sn.i is cap-closed semiring_of_sets of Xn.i
proof
let i be Nat;
assume
A14: i in Seg n;
then i in Seg len Xn & i in Seg len Sn by FINSEQ_3:153;
then X.i = (Xn ^ X1).i & S.i= (Sn ^ S1).i & 1 <= i & i <= len Xn &
i <= len Sn by A4,A10,FINSEQ_1:1;
then X.i = Xn.i & S.i = Sn.i by FINSEQ_1:64;
hence thesis by A14,A11,Def2,Def4;
end;
for i be Nat st i in Seg n holds
Sn.i is semiring_of_sets of Xn.i by A13;
then reconsider P=Sn as SemiringFamily of Xn by Def2;
P is cap-closed-yielding by A13;
hence Sn is cap-closed-yielding SemiringFamily of Xn;
end; then
A16: Xn is non-empty & Sn is cap-closed-yielding SemiringFamily of Xn &
SemiringProduct(Sn) is cap-closed semiring_of_sets of product Xn by A3;
A17: len X1 = 1 by FINSEQ_1:39; then
A18: X1.1 = X.(n+1) by FINSEQ_1:65,A4,A12;
len S1 = 1 by FINSEQ_1:39; then
A20: S1.1 = S.(n+1) by FINSEQ_1:65,A12,A10;
now
thus X1 is non-empty;
A23: n+1 in Seg (n+1) by FINSEQ_1:3;
A23a: now
let i be Nat;
assume i in Seg 1;
then i=1 by TARSKI:def 1,FINSEQ_1:2;
hence S1.i is cap-closed semiring_of_sets of X1.i
by A23,A20,A18,Def2,Def4;
end;
A23b: for i be Nat st i in Seg 1 holds
S1.i is semiring_of_sets of X1.i by A23a;
reconsider P=S1 as SemiringFamily of X1 by A23b,Def2;
for i be Nat st i in Seg 1 holds P.i is cap-closed by A23a;
hence X1.1=X.(n+1) &
S1 is cap-closed-yielding SemiringFamily of X1
by A17,FINSEQ_1:65,A4,A12,Def4;
end;
then
A24: S1 is cap-closed-yielding SemiringFamily of X1 &
SemiringProduct(S1) is cap-closed semiring_of_sets of product X1
by Thm34;
thus SemiringProduct(S) is cap-closed semiring_of_sets of product X
by A16,A24,Thm36,A10,A4;
end;
hence P[n + 1];
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
registration
let n, X;
let S be cap-closed-yielding SemiringFamily of X;
cluster SemiringProduct(S) -> cap-closed;
coherence by Thm37;
end;
:: Product of n classical semirings of sets is classical semiring of sets
theorem
for S being cap-closed-yielding SemiringFamily of X holds
SemiringProduct(S) is cap-closed semiring_of_sets of product X by Thm32;
begin :: Measurable Rectangle
:: n-classical semiring of sets
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
mode ClassicalSemiringFamily of X -> n-element FinSequence means
:Def5:
for i being Nat st i in Seg n holds
it.i is with_empty_element semi-diff-closed cap-closed Subset-Family of X.i;
existence
proof
deffunc F(set)=bool (X.$1);
consider p being FinSequence such that
A1: len p = n and
A2: for i being Nat st i in dom p holds p.i=F(i) from FINSEQ_1:sch 2;
reconsider p as n-element FinSequence by A1,CARD_1:def 7;
take p;
now
let i be Nat;
assume
A3: i in Seg n;
reconsider Xi=X.i as set;
bool Xi c= bool Xi;
then reconsider BXi=bool Xi as Subset-Family of Xi;
A4: BXi is cap-finite-partition-closed diff-c=-finite-partition-closed
with_countable_Cover with_empty_element Subset-Family of Xi;
i in dom p by A3,A1,FINSEQ_1:def 3;
hence p.i is with_empty_element semi-diff-closed
cap-closed Subset-Family of X.i by A2,A4;
end;
hence thesis;
end;
end;
:: Measurable rectangle
:: p148
:: Charalambos D. Aliprantis Kim C. Border
:: Infinite Dimensional Analysis
:: A Hitchhiker.s Guide Third Edition
:: Springer-Verlag Berlin Heidelberg 1999, 2006
::
:: Synonym SemiringProduct = MeasurableRectangle
::
:: This definition is similary of SemiringProduct
notation
let n be non zero Nat, X be n-element FinSequence;
synonym MeasurableRectangle(X) for SemiringProduct(X);
end;
theorem Thm38:
for S being ClassicalSemiringFamily of X holds
S is cap-closed-yielding SemiringFamily of X
proof
let S be ClassicalSemiringFamily of X;
now
let i be Nat;
assume
A1: i in Seg n;
S.i is with_empty_element semi-diff-closed cap-closed
Subset-Family of X.i by A1,Def5;
hence S.i is semiring_of_sets of X.i by SRINGS_3:9;
end;
then reconsider SC=S as SemiringFamily of X by Def2;
for i be Nat st i in Seg n holds SC.i is cap-closed by Def5;
hence thesis by Def4;
end;
:: finite product of classical semiring of sets is classical semiring of sets ::
:: Version SRING_3 ::
theorem
for S being ClassicalSemiringFamily of X holds
MeasurableRectangle(S) is
with_empty_element semi-diff-closed cap-closed Subset-Family of product X
proof
let S be ClassicalSemiringFamily of X;
reconsider S1=S as cap-closed-yielding SemiringFamily of X by Thm38;
SemiringProduct(S1) is cap-closed with_empty_element
cap-finite-partition-closed diff-finite-partition-closed
Subset-Family of product X by Thm32;
hence thesis by SRINGS_3:10;
end;