:: DYNKIN semantic presentation

theorem Th1: :: DYNKIN:1

for b₁ being non empty set
for b₂ being SetSequence of b₁
for b₃ being set holds
( b₃ in rng b₂ iff ex b₄ being Nat st b₂ . b₄ = b₃ )

proof end;

theorem Th2: :: DYNKIN:2

for b₁ being Nat holds PSeg b₁ is finite

proof end;

registration

let c₁ be Nat;
cluster PSeg a₁ -> finite ;
coherence by Th2;

end;

definition

let c₁, c₂, c₃ be set ;
func c₁,c₂ followed_by c₃ -> set equals :: DYNKIN:def 1
(NAT --> a₃) +* (0,1 --> a₁,a₂);
coherence ;

end;

:: deftheorem Def1 defines followed_by DYNKIN:def 1 :

registration

let c₁, c₂, c₃ be set ;
cluster a₁,a₂ followed_by a₃ -> Relation-like Function-like ;
coherence ;

end;

definition

let c₁ be non empty set ;
let c₂, c₃, c₄ be Element of c₁;
redefine func followed_by as c₂,c₃ followed_by c₄ -> Function of NAT ,a₁;
coherence

proof end;

end;

Lemma3: for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds b₂,b₃ followed_by b₄ is Function of NAT ,b₁
;

definition

let c₁ be non empty set ;
let c₂, c₃, c₄ be Subset of c₁;
redefine func followed_by as c₂,c₃ followed_by c₄ -> SetSequence of a₁;
coherence

proof end;

end;

theorem Th3: :: DYNKIN:3

canceled;

theorem Th4: :: DYNKIN:4

canceled;

theorem Th5: :: DYNKIN:5

for b₁, b₂, b₃ being set holds
( (b₁,b₂ followed_by b₃) . 0 = b₁ & (b₁,b₂ followed_by b₃) . 1 = b₂ & ( for b₄ being Nat st b₄ <> 0 & b₄ <> 1 holds
(b₁,b₂ followed_by b₃) . b₄ = b₃ ) )

proof end;

theorem Th6: :: DYNKIN:6

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ holds union (rng (b₂,b₃ followed_by {} )) = b₂ \/ b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be SetSequence of c₁;
let c₃ be Subset of c₁;
func seqIntersection c₃,c₂ -> SetSequence of a₁ means :Def2: :: DYNKIN:def 2
for b₁ being Nat holds a₄ . b₁ = a₃ /\ (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines seqIntersection DYNKIN:def 2 :

definition

let c₁ be non empty set ;
let c₂ be SetSequence of c₁;
redefine attr disjoint_valued as a₂ is disjoint_valued means :Def3: :: DYNKIN:def 3
for b₁, b₂ being Nat st b₁ < b₂ holds
a₂ . b₁ misses a₂ . b₂;
compatibility

proof end;

end;

:: deftheorem Def3 defines disjoint_valued DYNKIN:def 3 :

theorem Th7: :: DYNKIN:7

for b₁ being non empty set
for b₂ being set holds
( b₂ c= meet b₁ iff for b₃ being Element of b₁ holds b₂ c= b₃ )

proof end;

notation

let c₁ be set ;
synonym intersection_stable c₁ for multiplicative c₁;

end;

definition

let c₁ be non empty set ;
let c₂ be SetSequence of c₁;
let c₃ be Element of NAT ;
canceled;
func disjointify c₂,c₃ -> Subset of a₁ equals :: DYNKIN:def 5
(a₂ . a₃) \ (union (rng (a₂ | (PSeg a₃))));
coherence

proof end;

end;

:: deftheorem Def4 DYNKIN:def 4 :

:: deftheorem Def5 defines disjointify DYNKIN:def 5 :

definition

let c₁ be non empty set ;
let c₂ be SetSequence of c₁;
func disjointify c₂ -> SetSequence of a₁ means :Def6: :: DYNKIN:def 6
for b₁ being Nat holds a₃ . b₁ = disjointify a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines disjointify DYNKIN:def 6 :

theorem Th8: :: DYNKIN:8

for b₁ being non empty set
for b₂ being SetSequence of b₁
for b₃ being Nat holds (disjointify b₂) . b₃ = (b₂ . b₃) \ (union (rng (b₂ | (PSeg b₃))))

proof end;

theorem Th9: :: DYNKIN:9

for b₁ being non empty set
for b₂ being SetSequence of b₁ holds disjointify b₂ is disjoint_valued

proof end;

theorem Th10: :: DYNKIN:10

for b₁ being non empty set
for b₂ being SetSequence of b₁ holds union (rng (disjointify b₂)) = union (rng b₂)

proof end;

theorem Th11: :: DYNKIN:11

for b₁ being non empty set
for b₂, b₃ being Subset of b₁ st b₂ misses b₃ holds
b₂,b₃ followed_by ({} b₁) is disjoint_valued

proof end;

theorem Th12: :: DYNKIN:12

for b₁ being non empty set
for b₂ being SetSequence of b₁ st b₂ is disjoint_valued holds
for b₃ being Subset of b₁ holds seqIntersection b₃,b₂ is disjoint_valued

proof end;

theorem Th13: :: DYNKIN:13

for b₁ being non empty set
for b₂ being SetSequence of b₁
for b₃ being Subset of b₁ holds b₃ /\ (Union b₂) = Union (seqIntersection b₃,b₂)

proof end;

definition

let c₁ be non empty set ;
mode Dynkin_System of c₁ -> Subset-Family of a₁ means :Def7: :: DYNKIN:def 7
( ( for b₁ being SetSequence of a₁ st rng b₁ c= a₂ & b₁ is disjoint_valued holds
Union b₁ in a₂ ) & ( for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ ` in a₂ ) & {} in a₂ );
existence

proof end;

end;

:: deftheorem Def7 defines Dynkin_System DYNKIN:def 7 :

registration

let c₁ be non empty set ;
cluster -> non empty Dynkin_System of a₁;
coherence by Def7;

end;

theorem Th14: :: DYNKIN:14

for b₁ being non empty set holds bool b₁ is Dynkin_System of b₁

proof end;

theorem Th15: :: DYNKIN:15

for b₁, b₂ being non empty set st ( for b₃ being set st b₃ in b₁ holds
b₃ is Dynkin_System of b₂ ) holds
meet b₁ is Dynkin_System of b₂

proof end;

theorem Th16: :: DYNKIN:16

for b₁ being non empty set
for b₂, b₃ being Subset of b₁
for b₄ being non empty Subset-Family of b₁ st b₄ is Dynkin_System of b₁ & b₄ is intersection_stable & b₂ in b₄ & b₃ in b₄ holds
b₂ \ b₃ in b₄

proof end;

theorem Th17: :: DYNKIN:17

for b₁ being non empty set
for b₂, b₃ being Subset of b₁
for b₄ being non empty Subset-Family of b₁ st b₄ is Dynkin_System of b₁ & b₄ is intersection_stable & b₂ in b₄ & b₃ in b₄ holds
b₂ \/ b₃ in b₄

proof end;

theorem Th18: :: DYNKIN:18

for b₁ being non empty set
for b₂ being non empty Subset-Family of b₁ st b₂ is Dynkin_System of b₁ & b₂ is intersection_stable holds
for b₃ being finite set st b₃ c= b₂ holds
union b₃ in b₂

proof end;

theorem Th19: :: DYNKIN:19

for b₁ being non empty set
for b₂ being non empty Subset-Family of b₁ st b₂ is Dynkin_System of b₁ & b₂ is intersection_stable holds
for b₃ being SetSequence of b₁ st rng b₃ c= b₂ holds
rng (disjointify b₃) c= b₂

proof end;

theorem Th20: :: DYNKIN:20

for b₁ being non empty set
for b₂ being non empty Subset-Family of b₁ st b₂ is Dynkin_System of b₁ & b₂ is intersection_stable holds
for b₃ being SetSequence of b₁ st rng b₃ c= b₂ holds
union (rng b₃) in b₂

proof end;

theorem Th21: :: DYNKIN:21

for b₁ being non empty set
for b₂ being Dynkin_System of b₁
for b₃, b₄ being Element of b₂ st b₃ misses b₄ holds
b₃ \/ b₄ in b₂

proof end;

theorem Th22: :: DYNKIN:22

for b₁ being non empty set
for b₂ being Dynkin_System of b₁
for b₃, b₄ being Element of b₂ st b₃ c= b₄ holds
b₄ \ b₃ in b₂

proof end;

theorem Th23: :: DYNKIN:23

for b₁ being non empty set
for b₂ being non empty Subset-Family of b₁ st b₂ is Dynkin_System of b₁ & b₂ is intersection_stable holds
b₂ is SigmaField of b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
func generated_Dynkin_System c₂ -> Dynkin_System of a₁ means :Def8: :: DYNKIN:def 8
( a₂ c= a₃ & ( for b₁ being Dynkin_System of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines generated_Dynkin_System DYNKIN:def 8 :

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Subset of c₁;
func DynSys c₃,c₂ -> Subset-Family of a₁ means :Def9: :: DYNKIN:def 9
for b₁ being Subset of a₁ holds
( b₁ in a₄ iff b₁ /\ a₃ in a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines DynSys DYNKIN:def 9 :

definition

let c₁ be non empty set ;
let c₂ be Dynkin_System of c₁;
let c₃ be Element of c₂;
redefine func DynSys as DynSys c₃,c₂ -> Dynkin_System of a₁;
coherence

proof end;

end;

theorem Th24: :: DYNKIN:24

for b₁ being non empty set
for b₂ being Subset-Family of b₁
for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in generated_Dynkin_System b₂ & b₂ is intersection_stable holds
b₃ /\ b₄ in generated_Dynkin_System b₂

proof end;

theorem Th25: :: DYNKIN:25

for b₁ being non empty set
for b₂ being Subset-Family of b₁
for b₃, b₄ being Subset of b₁ st b₃ in generated_Dynkin_System b₂ & b₄ in generated_Dynkin_System b₂ & b₂ is intersection_stable holds
b₃ /\ b₄ in generated_Dynkin_System b₂

proof end;

theorem Th26: :: DYNKIN:26

for b₁ being non empty set
for b₂ being Subset-Family of b₁ st b₂ is intersection_stable holds
generated_Dynkin_System b₂ is intersection_stable

proof end;

theorem Th27: :: DYNKIN:27

for b₁ being non empty set
for b₂ being Subset-Family of b₁ st b₂ is intersection_stable holds
for b₃ being Dynkin_System of b₁ st b₂ c= b₃ holds
sigma b₂ c= b₃

proof end;