:: DYNKIN semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: DYNKIN:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Nat st f . n = x )
proof end;

theorem Th2: :: DYNKIN:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds PSeg n is finite
proof end;

registration
let n be Nat;
cluster PSeg n -> finite ;
coherence
PSeg n is finite
by Th2;
end;

definition
let a, b, c be set ;
func a,b followed_by c -> set equals :: DYNKIN:def 1
(NAT --> c) +* (0,1 --> a,b);
coherence
(NAT --> c) +* (0,1 --> a,b) is set
;
end;

:: deftheorem defines followed_by DYNKIN:def 1 :
for a, b, c being set holds a,b followed_by c = (NAT --> c) +* (0,1 --> a,b);

registration
let a, b, c be set ;
cluster a,b followed_by c -> Relation-like Function-like ;
coherence
( a,b followed_by c is Function-like & a,b followed_by c is Relation-like )
;
end;

definition
let X be non empty set ;
let a, b, c be Element of X;
:: original: followed_by
redefine func a,b followed_by c -> Function of NAT ,X;
coherence
a,b followed_by c is Function of NAT ,X
proof end;
end;

Lm1: for X being non empty set
for a, b, c being Element of X holds a,b followed_by c is Function of NAT ,X
;

definition
let Omega be non empty set ;
let a, b, c be Subset of Omega;
:: original: followed_by
redefine func a,b followed_by c -> SetSequence of Omega;
coherence
a,b followed_by c is SetSequence of Omega
proof end;
end;

theorem :: DYNKIN:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: DYNKIN:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: DYNKIN:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set holds
( (a,b followed_by c) . 0 = a & (a,b followed_by c) . 1 = b & ( for n being Nat st n <> 0 & n <> 1 holds
(a,b followed_by c) . n = c ) )
proof end;

theorem Th6: :: DYNKIN:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for a, b being Subset of Omega holds union (rng (a,b followed_by {} )) = a \/ b
proof end;

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
let X be Subset of Omega;
func seqIntersection X,f -> SetSequence of Omega means :Def2: :: DYNKIN:def 2
for n being Nat holds it . n = X /\ (f . n);
existence
ex b1 being SetSequence of Omega st
for n being Nat holds b1 . n = X /\ (f . n)
proof end;
uniqueness
for b1, b2 being SetSequence of Omega st ( for n being Nat holds b1 . n = X /\ (f . n) ) & ( for n being Nat holds b2 . n = X /\ (f . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines seqIntersection DYNKIN:def 2 :
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega
for b4 being SetSequence of Omega holds
( b4 = seqIntersection X,f iff for n being Nat holds b4 . n = X /\ (f . n) );

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
:: original: disjoint_valued
redefine attr f is disjoint_valued means :Def3: :: DYNKIN:def 3
for n, m being Nat st n < m holds
f . n misses f . m;
compatibility
( f is disjoint_valued iff for n, m being Nat st n < m holds
f . n misses f . m )
proof end;
end;

:: deftheorem Def3 defines disjoint_valued DYNKIN:def 3 :
for Omega being non empty set
for f being SetSequence of Omega holds
( f is disjoint_valued iff for n, m being Nat st n < m holds
f . n misses f . m );

theorem Th7: :: DYNKIN:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
proof end;

notation
let x be set ;
synonym intersection_stable x for multiplicative x;
end;

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
let n be Element of NAT ;
canceled;
func disjointify f,n -> Subset of Omega equals :: DYNKIN:def 5
(f . n) \ (union (rng (f | (PSeg n))));
coherence
(f . n) \ (union (rng (f | (PSeg n)))) is Subset of Omega
proof end;
end;

:: deftheorem DYNKIN:def 4 :
canceled;

:: deftheorem defines disjointify DYNKIN:def 5 :
for Omega being non empty set
for f being SetSequence of Omega
for n being Element of NAT holds disjointify f,n = (f . n) \ (union (rng (f | (PSeg n))));

definition
let Omega be non empty set ;
let g be SetSequence of Omega;
func disjointify g -> SetSequence of Omega means :Def6: :: DYNKIN:def 6
for n being Nat holds it . n = disjointify g,n;
existence
ex b1 being SetSequence of Omega st
for n being Nat holds b1 . n = disjointify g,n
proof end;
uniqueness
for b1, b2 being SetSequence of Omega st ( for n being Nat holds b1 . n = disjointify g,n ) & ( for n being Nat holds b2 . n = disjointify g,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines disjointify DYNKIN:def 6 :
for Omega being non empty set
for g, b3 being SetSequence of Omega holds
( b3 = disjointify g iff for n being Nat holds b3 . n = disjointify g,n );

theorem Th8: :: DYNKIN:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | (PSeg n))))
proof end;

theorem Th9: :: DYNKIN:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for f being SetSequence of Omega holds disjointify f is disjoint_valued
proof end;

theorem Th10: :: DYNKIN:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
proof end;

theorem Th11: :: DYNKIN:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for x, y being Subset of Omega st x misses y holds
x,y followed_by ({} Omega) is disjoint_valued
proof end;

theorem Th12: :: DYNKIN:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for f being SetSequence of Omega st f is disjoint_valued holds
for X being Subset of Omega holds seqIntersection X,f is disjoint_valued
proof end;

theorem Th13: :: DYNKIN:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection X,f)
proof end;

definition
let Omega be non empty set ;
mode Dynkin_System of Omega -> Subset-Family of Omega means :Def7: :: DYNKIN:def 7
( ( for f being SetSequence of Omega st rng f c= it & f is disjoint_valued holds
Union f in it ) & ( for X being Subset of Omega st X in it holds
X ` in it ) & {} in it );
existence
ex b1 being Subset-Family of Omega st
( ( for f being SetSequence of Omega st rng f c= b1 & f is disjoint_valued holds
Union f in b1 ) & ( for X being Subset of Omega st X in b1 holds
X ` in b1 ) & {} in b1 )
proof end;
end;

:: deftheorem Def7 defines Dynkin_System DYNKIN:def 7 :
for Omega being non empty set
for b2 being Subset-Family of Omega holds
( b2 is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b2 & f is disjoint_valued holds
Union f in b2 ) & ( for X being Subset of Omega st X in b2 holds
X ` in b2 ) & {} in b2 ) );

registration
let Omega be non empty set ;
cluster -> non empty Dynkin_System of Omega;
coherence
for b1 being Dynkin_System of Omega holds not b1 is empty
by Def7;
end;

theorem Th14: :: DYNKIN:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set holds bool Omega is Dynkin_System of Omega
proof end;

theorem Th15: :: DYNKIN:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, Omega being non empty set st ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) holds
meet F is Dynkin_System of Omega
proof end;

theorem Th16: :: DYNKIN:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
proof end;

theorem Th17: :: DYNKIN:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
proof end;

theorem Th18: :: DYNKIN:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
proof end;

theorem Th19: :: DYNKIN:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
proof end;

theorem Th20: :: DYNKIN:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
proof end;

theorem Th21: :: DYNKIN:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
proof end;

theorem Th22: :: DYNKIN:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
proof end;

theorem Th23: :: DYNKIN:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega
proof end;

definition
let Omega be non empty set ;
let E be Subset-Family of Omega;
func generated_Dynkin_System E -> Dynkin_System of Omega means :Def8: :: DYNKIN:def 8
( E c= it & ( for D being Dynkin_System of Omega st E c= D holds
it c= D ) );
existence
ex b1 being Dynkin_System of Omega st
( E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being Dynkin_System of Omega st E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) & E c= b2 & ( for D being Dynkin_System of Omega st E c= D holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines generated_Dynkin_System DYNKIN:def 8 :
for Omega being non empty set
for E being Subset-Family of Omega
for b3 being Dynkin_System of Omega holds
( b3 = generated_Dynkin_System E iff ( E c= b3 & ( for D being Dynkin_System of Omega st E c= D holds
b3 c= D ) ) );

definition
let Omega be non empty set ;
let G be set ;
let X be Subset of Omega;
func DynSys X,G -> Subset-Family of Omega means :Def9: :: DYNKIN:def 9
for A being Subset of Omega holds
( A in it iff A /\ X in G );
existence
ex b1 being Subset-Family of Omega st
for A being Subset of Omega holds
( A in b1 iff A /\ X in G )
proof end;
uniqueness
for b1, b2 being Subset-Family of Omega st ( for A being Subset of Omega holds
( A in b1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in b2 iff A /\ X in G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines DynSys DYNKIN:def 9 :
for Omega being non empty set
for G being set
for X being Subset of Omega
for b4 being Subset-Family of Omega holds
( b4 = DynSys X,G iff for A being Subset of Omega holds
( A in b4 iff A /\ X in G ) );

definition
let Omega be non empty set ;
let G be Dynkin_System of Omega;
let X be Element of G;
:: original: DynSys
redefine func DynSys X,G -> Dynkin_System of Omega;
coherence
DynSys X,G is Dynkin_System of Omega
proof end;
end;

theorem Th24: :: DYNKIN:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proof end;

theorem Th25: :: DYNKIN:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proof end;

theorem Th26: :: DYNKIN:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
proof end;

theorem :: DYNKIN:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
proof end;