:: by Krzysztof Retel

::

:: Received February 3, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

theorem Th3: :: NECKLA_3:3

for a, b, c, d, e, f, g, h being set holds [:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}

proof end;

registration

let X, Y be trivial set ;

correctness

coherence

for b_{1} being Relation of X,Y holds b_{1} is trivial ;

;

end;
correctness

coherence

for b

;

theorem Th4: :: NECKLA_3:4

for X being trivial set

for R being Relation of X st not R is empty holds

ex x being object st R = {[x,x]}

for R being Relation of X st not R is empty holds

ex x being object st R = {[x,x]}

proof end;

registration

let X be trivial set ;

correctness

coherence

for b_{1} being Relation of X holds

( b_{1} is trivial & b_{1} is reflexive & b_{1} is symmetric & b_{1} is transitive & b_{1} is strongly_connected );

end;
correctness

coherence

for b

( b

proof end;

registration

correctness

existence

ex b_{1} being RelStr st

( not b_{1} is empty & b_{1} is strict & b_{1} is finite & b_{1} is irreflexive & b_{1} is symmetric );

end;
existence

ex b

( not b

proof end;

registration

let L be irreflexive RelStr ;

correctness

coherence

for b_{1} being full SubRelStr of L holds b_{1} is irreflexive ;

end;
correctness

coherence

for b

proof end;

registration

let L be symmetric RelStr ;

correctness

coherence

for b_{1} being full SubRelStr of L holds b_{1} is symmetric ;

end;
correctness

coherence

for b

proof end;

theorem Th6: :: NECKLA_3:6

for R being symmetric irreflexive RelStr st card the carrier of R = 2 holds

ex a, b being object st

( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

ex a, b being object st

( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

proof end;

registration

let R be non empty RelStr ;

let S be RelStr ;

correctness

coherence

not union_of (R,S) is empty ;

coherence

not sum_of (R,S) is empty ;

end;
let S be RelStr ;

correctness

coherence

not union_of (R,S) is empty ;

proof end;

correctness coherence

not sum_of (R,S) is empty ;

proof end;

registration

let R be RelStr ;

let S be non empty RelStr ;

correctness

coherence

not union_of (R,S) is empty ;

coherence

not sum_of (R,S) is empty ;

end;
let S be non empty RelStr ;

correctness

coherence

not union_of (R,S) is empty ;

proof end;

correctness coherence

not sum_of (R,S) is empty ;

proof end;

registration

let R, S be finite RelStr ;

correctness

coherence

union_of (R,S) is finite ;

coherence

sum_of (R,S) is finite ;

end;
correctness

coherence

union_of (R,S) is finite ;

proof end;

correctness coherence

sum_of (R,S) is finite ;

proof end;

registration

let R, S be symmetric RelStr ;

correctness

coherence

union_of (R,S) is symmetric ;

coherence

sum_of (R,S) is symmetric ;

end;
correctness

coherence

union_of (R,S) is symmetric ;

proof end;

correctness coherence

sum_of (R,S) is symmetric ;

proof end;

registration
end;

theorem :: NECKLA_3:7

for R, S being irreflexive RelStr st the carrier of R misses the carrier of S holds

sum_of (R,S) is irreflexive

sum_of (R,S) is irreflexive

proof end;

theorem Th8: :: NECKLA_3:8

for R1, R2 being RelStr holds

( union_of (R1,R2) = union_of (R2,R1) & sum_of (R1,R2) = sum_of (R2,R1) )

( union_of (R1,R2) = union_of (R2,R1) & sum_of (R1,R2) = sum_of (R2,R1) )

proof end;

theorem Th9: :: NECKLA_3:9

for G being irreflexive RelStr

for G1, G2 being RelStr st ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) holds

( G1 is irreflexive & G2 is irreflexive )

for G1, G2 being RelStr st ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) holds

( G1 is irreflexive & G2 is irreflexive )

proof end;

theorem Th10: :: NECKLA_3:10

for G being non empty RelStr

for H1, H2 being RelStr st the carrier of H1 misses the carrier of H2 & ( RelStr(# the carrier of G, the InternalRel of G #) = union_of (H1,H2) or RelStr(# the carrier of G, the InternalRel of G #) = sum_of (H1,H2) ) holds

( H1 is full SubRelStr of G & H2 is full SubRelStr of G )

for H1, H2 being RelStr st the carrier of H1 misses the carrier of H2 & ( RelStr(# the carrier of G, the InternalRel of G #) = union_of (H1,H2) or RelStr(# the carrier of G, the InternalRel of G #) = sum_of (H1,H2) ) holds

( H1 is full SubRelStr of G & H2 is full SubRelStr of G )

proof end;

registration
end;

theorem Th14: :: NECKLA_3:14

for G being RelStr holds [: the carrier of G, the carrier of G:] = ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)

proof end;

theorem Th17: :: NECKLA_3:17

for G1, G2 being RelStr st the carrier of G1 misses the carrier of G2 holds

ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2))

ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2))

proof end;

theorem Th18: :: NECKLA_3:18

for G1, G2 being RelStr st the carrier of G1 misses the carrier of G2 holds

ComplRelStr (sum_of (G1,G2)) = union_of ((ComplRelStr G1),(ComplRelStr G2))

ComplRelStr (sum_of (G1,G2)) = union_of ((ComplRelStr G1),(ComplRelStr G2))

proof end;

theorem :: NECKLA_3:19

for G being RelStr

for H being full SubRelStr of G holds the InternalRel of (ComplRelStr H) = the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H)

for H being full SubRelStr of G holds the InternalRel of (ComplRelStr H) = the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H)

proof end;

theorem Th20: :: NECKLA_3:20

for G being non empty irreflexive RelStr

for x being Element of G

for x9 being Element of (ComplRelStr G) st x = x9 holds

ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})

for x being Element of G

for x9 being Element of (ComplRelStr G) st x = x9 holds

ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})

proof end;

registration

correctness

coherence

for b_{1} being non empty RelStr st b_{1} is trivial & b_{1} is strict holds

b_{1} is N-free ;

end;
coherence

for b

b

proof end;

theorem :: NECKLA_3:21

for R being reflexive antisymmetric RelStr

for S being RelStr holds

( ex f being Function of R,S st

for x, y being Element of R holds

( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )

for S being RelStr holds

( ex f being Function of R,S st

for x, y being Element of R holds

( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )

proof end;

theorem Th23: :: NECKLA_3:23

for G being non empty RelStr

for H being non empty full SubRelStr of G st G is N-free holds

H is N-free

for H being non empty full SubRelStr of G st G is N-free holds

H is N-free

proof end;

theorem Th24: :: NECKLA_3:24

for G being non empty irreflexive RelStr holds

( G embeds Necklace 4 iff ComplRelStr G embeds Necklace 4 )

( G embeds Necklace 4 iff ComplRelStr G embeds Necklace 4 )

proof end;

definition

let R be RelStr ;

end;
attr R is path-connected means :: NECKLA_3:def 1

for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x;

for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x;

:: deftheorem defines path-connected NECKLA_3:def 1 :

for R being RelStr holds

( R is path-connected iff for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x );

for R being RelStr holds

( R is path-connected iff for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x );

registration
end;

registration

correctness

coherence

for b_{1} being non empty RelStr st b_{1} is connected holds

b_{1} is path-connected ;

end;
coherence

for b

b

proof end;

theorem Th26: :: NECKLA_3:26

for R being non empty reflexive transitive RelStr

for x, y being Element of R st the InternalRel of R reduces x,y holds

[x,y] in the InternalRel of R

for x, y being Element of R st the InternalRel of R reduces x,y holds

[x,y] in the InternalRel of R

proof end;

registration

coherence

for b_{1} being non empty reflexive transitive RelStr st b_{1} is path-connected holds

b_{1} is connected ;

end;

cluster non empty reflexive transitive path-connected -> non empty reflexive transitive connected for RelStr ;

correctness coherence

for b

b

proof end;

theorem Th27: :: NECKLA_3:27

for R being symmetric RelStr

for x, y being set st the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x

for x, y being set st the InternalRel of R reduces x,y holds

the InternalRel of R reduces y,x

proof end;

definition

let R be symmetric RelStr ;

( R is path-connected iff for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds

the InternalRel of R reduces x,y )

end;
redefine attr R is path-connected means :: NECKLA_3:def 2

for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds

the InternalRel of R reduces x,y;

compatibility for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds

the InternalRel of R reduces x,y;

( R is path-connected iff for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds

the InternalRel of R reduces x,y )

proof end;

:: deftheorem defines path-connected NECKLA_3:def 2 :

for R being symmetric RelStr holds

( R is path-connected iff for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds

the InternalRel of R reduces x,y );

for R being symmetric RelStr holds

( R is path-connected iff for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds

the InternalRel of R reduces x,y );

definition

let R be RelStr ;

let x be Element of R;

coherence

Class ((EqCl the InternalRel of R),x) is Subset of R ;

end;
let x be Element of R;

coherence

Class ((EqCl the InternalRel of R),x) is Subset of R ;

:: deftheorem defines component NECKLA_3:def 3 :

for R being RelStr

for x being Element of R holds component x = Class ((EqCl the InternalRel of R),x);

for R being RelStr

for x being Element of R holds component x = Class ((EqCl the InternalRel of R),x);

registration

let R be non empty RelStr ;

let x be Element of R;

correctness

coherence

not component x is empty ;

by EQREL_1:20;

end;
let x be Element of R;

correctness

coherence

not component x is empty ;

by EQREL_1:20;

theorem Th28: :: NECKLA_3:28

for R being RelStr

for x being Element of R

for y being set st y in component x holds

[x,y] in EqCl the InternalRel of R

for x being Element of R

for y being set st y in component x holds

[x,y] in EqCl the InternalRel of R

proof end;

theorem Th29: :: NECKLA_3:29

for R being RelStr

for x being Element of R

for A being set holds

( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

for x being Element of R

for A being set holds

( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

proof end;

theorem Th30: :: NECKLA_3:30

for R being non empty symmetric irreflexive RelStr st not R is path-connected holds

ex G1, G2 being non empty strict symmetric irreflexive RelStr st

( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = union_of (G1,G2) )

ex G1, G2 being non empty strict symmetric irreflexive RelStr st

( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = union_of (G1,G2) )

proof end;

theorem Th31: :: NECKLA_3:31

for R being non empty symmetric irreflexive RelStr st not ComplRelStr R is path-connected holds

ex G1, G2 being non empty strict symmetric irreflexive RelStr st

( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = sum_of (G1,G2) )

ex G1, G2 being non empty strict symmetric irreflexive RelStr st

( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = sum_of (G1,G2) )

proof end;

Lm1: for X being non empty finite set

for A, B being non empty set st X = A \/ B & A misses B holds

card A in Segm (card X)

proof end;

theorem Th33: :: NECKLA_3:33

for R being symmetric irreflexive RelStr st card the carrier of R = 2 & the carrier of R in FinSETS holds

RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp

RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp

proof end;

theorem Th35: :: NECKLA_3:35

for G being RelStr

for H1, H2 being non empty RelStr

for x being Element of H1

for y being Element of H2 st G = union_of (H1,H2) & the carrier of H1 misses the carrier of H2 holds

not [x,y] in the InternalRel of G

for H1, H2 being non empty RelStr

for x being Element of H1

for y being Element of H2 st G = union_of (H1,H2) & the carrier of H1 misses the carrier of H2 holds

not [x,y] in the InternalRel of G

proof end;

theorem :: NECKLA_3:36

for G being RelStr

for H1, H2 being non empty RelStr

for x being Element of H1

for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

for H1, H2 being non empty RelStr

for x being Element of H1

for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

proof end;

theorem Th37: :: NECKLA_3:37

for G being non empty symmetric RelStr

for x being Element of G

for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & G is path-connected holds

ex b being Element of R1 st [b,x] in the InternalRel of G

for x being Element of G

for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & G is path-connected holds

ex b being Element of R1 st [b,x] in the InternalRel of G

proof end;

theorem Th38: :: NECKLA_3:38

for G being non empty symmetric irreflexive RelStr

for a, b, c, d being Element of G

for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds

subrelstr Z embeds Necklace 4

for a, b, c, d being Element of G

for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds

subrelstr Z embeds Necklace 4

proof end;

theorem Th39: :: NECKLA_3:39

for G being non empty symmetric irreflexive RelStr

for x being Element of G

for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds

G embeds Necklace 4

for x being Element of G

for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds

G embeds Necklace 4

proof end;

theorem :: NECKLA_3:40

for G being non empty finite strict symmetric irreflexive RelStr st G is N-free & the carrier of G in FinSETS holds

RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp

RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp

proof end;