:: by Piotr Rudnicki

::

:: Received September 17, 2009

:: Copyright (c) 2009-2016 Association of Mizar Users

:: Facts that I could not find in MML.

theorem Th2: :: DILWORTH:2

for X, Y being set

for F being Subset-Family of X

for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)

for F being Subset-Family of X

for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)

proof end;

theorem Th3: :: DILWORTH:3

for X, Y being set

for F being a_partition of X

for G being a_partition of Y st X misses Y holds

F \/ G is a_partition of X \/ Y

for F being a_partition of X

for G being a_partition of Y st X misses Y holds

F \/ G is a_partition of X \/ Y

proof end;

:: deftheorem Def1 defines connected DILWORTH:def 1 :

for R being RelStr

for S being Subset of R holds

( S is connected iff the InternalRel of R is_connected_in S );

for R being RelStr

for S being Subset of R holds

( S is connected iff the InternalRel of R is_connected_in S );

registration

let R be RelStr ;

coherence

for b_{1} being Subset of R st b_{1} is trivial holds

b_{1} is clique

end;
coherence

for b

b

proof end;

registration
end;

theorem Th6: :: DILWORTH:6

for R being RelStr

for S being Subset of R holds

( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds

b <= a )

for S being Subset of R holds

( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds

b <= a )

proof end;

registration
end;

registration

let R be reflexive RelStr ;

coherence

for b_{1} being Subset of R st b_{1} is connected holds

b_{1} is strongly_connected

end;
coherence

for b

b

proof end;

registration

let R be non empty RelStr ;

existence

ex b_{1} being Clique of R st

( b_{1} is finite & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

theorem :: DILWORTH:7

for R being non empty RelStr

for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds

a2 <= a1

for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds

a2 <= a1

proof end;

theorem Th8: :: DILWORTH:8

for R being non empty RelStr

for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds

{a1,a2} is Clique of R

for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds

{a1,a2} is Clique of R

proof end;

theorem :: DILWORTH:10

for R being RelStr

for C being finite Clique of R

for n being Nat st n <= card C holds

ex B being finite Clique of R st

( B c= C & card B = n )

for C being finite Clique of R

for n being Nat st n <= card C holds

ex B being finite Clique of R st

( B c= C & card B = n )

proof end;

theorem Th11: :: DILWORTH:11

for R being transitive RelStr

for C being Clique of R

for x, y being Element of R st x is_maximal_in C & x <= y holds

C \/ {y} is Clique of R

for C being Clique of R

for x, y being Element of R st x is_maximal_in C & x <= y holds

C \/ {y} is Clique of R

proof end;

theorem Th12: :: DILWORTH:12

for R being transitive RelStr

for C being Clique of R

for x, y being Element of R st x is_minimal_in C & y <= x holds

C \/ {y} is Clique of R

for C being Clique of R

for x, y being Element of R st x is_minimal_in C & y <= x holds

C \/ {y} is Clique of R

proof end;

:: deftheorem Def2 defines stable DILWORTH:def 2 :

for R being RelStr

for S being Subset of R holds

( S is stable iff for x, y being Element of R st x in S & y in S & x <> y holds

( not x <= y & not y <= x ) );

for R being RelStr

for S being Subset of R holds

( S is stable iff for x, y being Element of R st x in S & y in S & x <> y holds

( not x <= y & not y <= x ) );

registration

let R be RelStr ;

coherence

for b_{1} being Subset of R st b_{1} is trivial holds

b_{1} is stable
by ZFMISC_1:def 10;

end;
coherence

for b

b

registration
end;

registration
end;

registration

let R be non empty RelStr ;

existence

ex b_{1} being StableSet of R st

( b_{1} is finite & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

theorem :: DILWORTH:13

for R being non empty RelStr

for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds

( not a1 <= a2 & not a2 <= a1 )

for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds

( not a1 <= a2 & not a2 <= a1 )

proof end;

theorem Th14: :: DILWORTH:14

for R being non empty RelStr

for a1, a2 being Element of R holds

( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )

for a1, a2 being Element of R holds

( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )

proof end;

theorem Th15: :: DILWORTH:15

for R being RelStr

for C being Clique of R

for A being StableSet of R

for a, b being set st a in A & b in A & a in C & b in C holds

a = b

for C being Clique of R

for A being StableSet of R

for a, b being set st a in A & b in A & a in C & b in C holds

a = b

proof end;

theorem Th17: :: DILWORTH:17

for R being RelStr

for A being finite StableSet of R

for n being Nat st n <= card A holds

ex B being finite StableSet of R st card B = n

for A being finite StableSet of R

for n being Nat st n <= card A holds

ex B being finite StableSet of R st card B = n

proof end;

definition

let R be RelStr ;

end;
attr R is with_finite_clique# means :Def3: :: DILWORTH:def 3

ex C being finite Clique of R st

for D being finite Clique of R holds card D <= card C;

ex C being finite Clique of R st

for D being finite Clique of R holds card D <= card C;

:: deftheorem Def3 defines with_finite_clique# DILWORTH:def 3 :

for R being RelStr holds

( R is with_finite_clique# iff ex C being finite Clique of R st

for D being finite Clique of R holds card D <= card C );

for R being RelStr holds

( R is with_finite_clique# iff ex C being finite Clique of R st

for D being finite Clique of R holds card D <= card C );

registration
end;

registration

let R be with_finite_clique# RelStr ;

coherence

for b_{1} being Clique of R holds b_{1} is finite

end;
coherence

for b

proof end;

definition

let R be with_finite_clique# RelStr ;

ex b_{1} being Nat st

( ex C being finite Clique of R st card C = b_{1} & ( for T being finite Clique of R holds card T <= b_{1} ) )

for b_{1}, b_{2} being Nat st ex C being finite Clique of R st card C = b_{1} & ( for T being finite Clique of R holds card T <= b_{1} ) & ex C being finite Clique of R st card C = b_{2} & ( for T being finite Clique of R holds card T <= b_{2} ) holds

b_{1} = b_{2}

end;
func clique# R -> Nat means :Def4: :: DILWORTH:def 4

( ex C being finite Clique of R st card C = it & ( for T being finite Clique of R holds card T <= it ) );

existence ( ex C being finite Clique of R st card C = it & ( for T being finite Clique of R holds card T <= it ) );

ex b

( ex C being finite Clique of R st card C = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines clique# DILWORTH:def 4 :

for R being with_finite_clique# RelStr

for b_{2} being Nat holds

( b_{2} = clique# R iff ( ex C being finite Clique of R st card C = b_{2} & ( for T being finite Clique of R holds card T <= b_{2} ) ) );

for R being with_finite_clique# RelStr

for b

( b

registration
end;

registration
end;

definition

let R be RelStr ;

end;
attr R is with_finite_stability# means :Def5: :: DILWORTH:def 5

ex A being finite StableSet of R st

for B being finite StableSet of R holds card B <= card A;

ex A being finite StableSet of R st

for B being finite StableSet of R holds card B <= card A;

:: deftheorem Def5 defines with_finite_stability# DILWORTH:def 5 :

for R being RelStr holds

( R is with_finite_stability# iff ex A being finite StableSet of R st

for B being finite StableSet of R holds card B <= card A );

for R being RelStr holds

( R is with_finite_stability# iff ex A being finite StableSet of R st

for B being finite StableSet of R holds card B <= card A );

registration

coherence

for b_{1} being RelStr st b_{1} is finite holds

b_{1} is with_finite_stability#

end;
for b

b

proof end;

registration

let R be with_finite_stability# RelStr ;

coherence

for b_{1} being StableSet of R holds b_{1} is finite

end;
coherence

for b

proof end;

definition

let R be with_finite_stability# RelStr ;

ex b_{1} being Nat st

( ex A being finite StableSet of R st card A = b_{1} & ( for T being finite StableSet of R holds card T <= b_{1} ) )

for b_{1}, b_{2} being Nat st ex A being finite StableSet of R st card A = b_{1} & ( for T being finite StableSet of R holds card T <= b_{1} ) & ex A being finite StableSet of R st card A = b_{2} & ( for T being finite StableSet of R holds card T <= b_{2} ) holds

b_{1} = b_{2}

end;
func stability# R -> Nat means :Def6: :: DILWORTH:def 6

( ex A being finite StableSet of R st card A = it & ( for T being finite StableSet of R holds card T <= it ) );

existence ( ex A being finite StableSet of R st card A = it & ( for T being finite StableSet of R holds card T <= it ) );

ex b

( ex A being finite StableSet of R st card A = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines stability# DILWORTH:def 6 :

for R being with_finite_stability# RelStr

for b_{2} being Nat holds

( b_{2} = stability# R iff ( ex A being finite StableSet of R st card A = b_{2} & ( for T being finite StableSet of R holds card T <= b_{2} ) ) );

for R being with_finite_stability# RelStr

for b

( b

registration
end;

registration
end;

registration

coherence

for b_{1} being RelStr st b_{1} is with_finite_clique# & b_{1} is with_finite_stability# holds

b_{1} is finite

end;
for b

b

proof end;

definition

let R be RelStr ;

let X be Subset of R;

coherence

X \/ (downarrow X) is Subset of R ;

coherence

X \/ (uparrow X) is Subset of R ;

end;
let X be Subset of R;

coherence

X \/ (downarrow X) is Subset of R ;

coherence

X \/ (uparrow X) is Subset of R ;

:: deftheorem defines Lower DILWORTH:def 7 :

for R being RelStr

for X being Subset of R holds Lower X = X \/ (downarrow X);

for R being RelStr

for X being Subset of R holds Lower X = X \/ (downarrow X);

:: deftheorem defines Upper DILWORTH:def 8 :

for R being RelStr

for X being Subset of R holds Upper X = X \/ (uparrow X);

for R being RelStr

for X being Subset of R holds Upper X = X \/ (uparrow X);

theorem Th22: :: DILWORTH:22

for R being transitive antisymmetric RelStr

for A being StableSet of R

for z being set st z in Upper A & z in Lower A holds

z in A

for A being StableSet of R

for z being set st z in Upper A & z in Lower A holds

z in A

proof end;

theorem Th23: :: DILWORTH:23

for R being with_finite_stability# RelStr

for A being StableSet of R st card A = stability# R holds

(Upper A) \/ (Lower A) = [#] R

for A being StableSet of R st card A = stability# R holds

(Upper A) \/ (Lower A) = [#] R

proof end;

theorem Th24: :: DILWORTH:24

for R being transitive RelStr

for x being Element of R

for S being Subset of R st x is_minimal_in Lower S holds

x is_minimal_in [#] R

for x being Element of R

for S being Subset of R st x is_minimal_in Lower S holds

x is_minimal_in [#] R

proof end;

theorem Th25: :: DILWORTH:25

for R being transitive RelStr

for x being Element of R

for S being Subset of R st x is_maximal_in Upper S holds

x is_maximal_in [#] R

for x being Element of R

for S being Subset of R st x is_maximal_in Upper S holds

x is_maximal_in [#] R

proof end;

definition

let R be RelStr ;

set cR = the carrier of R;

for b_{1} being Subset of R holds verum
;

existence

( ( not R is empty implies ex b_{1} being Subset of R st

for x being Element of R holds

( x in b_{1} iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b_{1} being Subset of R st b_{1} = {} ) )

for b_{1}, b_{2} being Subset of R holds

( ( not R is empty & ( for x being Element of R holds

( x in b_{1} iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds

( x in b_{2} iff x is_minimal_in [#] R ) ) implies b_{1} = b_{2} ) & ( R is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being Subset of R holds verum
;

existence

( ( not R is empty implies ex b_{1} being Subset of R st

for x being Element of R holds

( x in b_{1} iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b_{1} being Subset of R st b_{1} = {} ) )

for b_{1}, b_{2} being Subset of R holds

( ( not R is empty & ( for x being Element of R holds

( x in b_{1} iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds

( x in b_{2} iff x is_maximal_in [#] R ) ) implies b_{1} = b_{2} ) & ( R is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

end;
set cR = the carrier of R;

func minimals R -> Subset of R means :Def9: :: DILWORTH:def 9

for x being Element of R holds

( x in it iff x is_minimal_in [#] R ) if not R is empty

otherwise it = {} ;

consistency for x being Element of R holds

( x in it iff x is_minimal_in [#] R ) if not R is empty

otherwise it = {} ;

for b

existence

( ( not R is empty implies ex b

for x being Element of R holds

( x in b

proof end;

uniqueness for b

( ( not R is empty & ( for x being Element of R holds

( x in b

( x in b

proof end;

func maximals R -> Subset of R means :Def10: :: DILWORTH:def 10

for x being Element of R holds

( x in it iff x is_maximal_in [#] R ) if not R is empty

otherwise it = {} ;

consistency for x being Element of R holds

( x in it iff x is_maximal_in [#] R ) if not R is empty

otherwise it = {} ;

for b

existence

( ( not R is empty implies ex b

for x being Element of R holds

( x in b

proof end;

uniqueness for b

( ( not R is empty & ( for x being Element of R holds

( x in b

( x in b

proof end;

:: deftheorem Def9 defines minimals DILWORTH:def 9 :

for R being RelStr

for b_{2} being Subset of R holds

( ( not R is empty implies ( b_{2} = minimals R iff for x being Element of R holds

( x in b_{2} iff x is_minimal_in [#] R ) ) ) & ( R is empty implies ( b_{2} = minimals R iff b_{2} = {} ) ) );

for R being RelStr

for b

( ( not R is empty implies ( b

( x in b

:: deftheorem Def10 defines maximals DILWORTH:def 10 :

for R being RelStr

for b_{2} being Subset of R holds

( ( not R is empty implies ( b_{2} = maximals R iff for x being Element of R holds

( x in b_{2} iff x is_maximal_in [#] R ) ) ) & ( R is empty implies ( b_{2} = maximals R iff b_{2} = {} ) ) );

for R being RelStr

for b

( ( not R is empty implies ( b

( x in b

registration

let R be non empty transitive antisymmetric with_finite_clique# RelStr ;

coherence

not maximals R is empty

not minimals R is empty

end;
coherence

not maximals R is empty

proof end;

coherence not minimals R is empty

proof end;

registration

let R be RelStr ;

coherence

minimals R is stable

maximals R is stable

end;
coherence

minimals R is stable

proof end;

coherence maximals R is stable

proof end;

theorem Th26: :: DILWORTH:26

for R being RelStr

for A being StableSet of R st not minimals R c= A holds

not minimals R c= Upper A

for A being StableSet of R st not minimals R c= A holds

not minimals R c= Upper A

proof end;

theorem Th27: :: DILWORTH:27

for R being RelStr

for A being StableSet of R st not maximals R c= A holds

not maximals R c= Lower A

for A being StableSet of R st not maximals R c= A holds

not maximals R c= Lower A

proof end;

registration
end;

theorem Th28: :: DILWORTH:28

for R being RelStr

for S being Subset of R

for C being Clique of (subrelstr S) holds C is Clique of R

for S being Subset of R

for C being Clique of (subrelstr S) holds C is Clique of R

proof end;

theorem Th29: :: DILWORTH:29

for R being RelStr

for S being Subset of R

for C being Clique of R holds C /\ S is Clique of (subrelstr S)

for S being Subset of R

for C being Clique of R holds C /\ S is Clique of (subrelstr S)

proof end;

theorem Th30: :: DILWORTH:30

for R being RelStr

for S being Subset of R

for A being StableSet of (subrelstr S) holds A is StableSet of R

for S being Subset of R

for A being StableSet of (subrelstr S) holds A is StableSet of R

proof end;

theorem Th31: :: DILWORTH:31

for R being RelStr

for S being Subset of R

for A being StableSet of R holds A /\ S is StableSet of (subrelstr S)

for S being Subset of R

for A being StableSet of R holds A /\ S is StableSet of (subrelstr S)

proof end;

theorem Th32: :: DILWORTH:32

for R being RelStr

for S being Subset of R

for B being Subset of (subrelstr S)

for x being Element of (subrelstr S)

for y being Element of R st x = y & x is_maximal_in B holds

y is_maximal_in B

for S being Subset of R

for B being Subset of (subrelstr S)

for x being Element of (subrelstr S)

for y being Element of R st x = y & x is_maximal_in B holds

y is_maximal_in B

proof end;

theorem Th33: :: DILWORTH:33

for R being RelStr

for S being Subset of R

for B being Subset of (subrelstr S)

for x being Element of (subrelstr S)

for y being Element of R st x = y & x is_minimal_in B holds

y is_minimal_in B

for S being Subset of R

for B being Subset of (subrelstr S)

for x being Element of (subrelstr S)

for y being Element of R st x = y & x is_minimal_in B holds

y is_minimal_in B

proof end;

theorem Th34: :: DILWORTH:34

for R being transitive RelStr

for A being StableSet of R

for C being Clique of (subrelstr (Lower A))

for a, b being Element of R st a in A & a in C & b in C & not a = b holds

b <= a

for A being StableSet of R

for C being Clique of (subrelstr (Lower A))

for a, b being Element of R st a in A & a in C & b in C & not a = b holds

b <= a

proof end;

theorem Th35: :: DILWORTH:35

for R being transitive RelStr

for A being StableSet of R

for C being Clique of (subrelstr (Upper A))

for a, b being Element of R st a in A & a in C & b in C & not a = b holds

a <= b

for A being StableSet of R

for C being Clique of (subrelstr (Upper A))

for a, b being Element of R st a in A & a in C & b in C & not a = b holds

a <= b

proof end;

registration

let R be with_finite_clique# RelStr ;

let S be Subset of R;

coherence

subrelstr S is with_finite_clique#

end;
let S be Subset of R;

coherence

subrelstr S is with_finite_clique#

proof end;

registration

let R be with_finite_stability# RelStr ;

let S be Subset of R;

coherence

subrelstr S is with_finite_stability#

end;
let S be Subset of R;

coherence

subrelstr S is with_finite_stability#

proof end;

theorem Th36: :: DILWORTH:36

for R being non empty transitive antisymmetric with_finite_clique# RelStr

for x being Element of R ex y being Element of R st

( y is_minimal_in [#] R & ( y = x or y < x ) )

for x being Element of R ex y being Element of R st

( y is_minimal_in [#] R & ( y = x or y < x ) )

proof end;

theorem Th38: :: DILWORTH:38

for R being non empty transitive antisymmetric with_finite_clique# RelStr

for x being Element of R ex y being Element of R st

( y is_maximal_in [#] R & ( y = x or x < y ) )

for x being Element of R ex y being Element of R st

( y is_maximal_in [#] R & ( y = x or x < y ) )

proof end;

theorem Th40: :: DILWORTH:40

for R being transitive antisymmetric with_finite_clique# RelStr

for A being StableSet of R st minimals R c= A holds

A = minimals R

for A being StableSet of R st minimals R c= A holds

A = minimals R

proof end;

theorem Th41: :: DILWORTH:41

for R being transitive antisymmetric with_finite_clique# RelStr

for A being StableSet of R st maximals R c= A holds

A = maximals R

for A being StableSet of R st maximals R c= A holds

A = maximals R

proof end;

theorem Th42: :: DILWORTH:42

for R being with_finite_clique# RelStr

for S being Subset of R holds clique# (subrelstr S) <= clique# R

for S being Subset of R holds clique# (subrelstr S) <= clique# R

proof end;

theorem :: DILWORTH:43

for R being with_finite_clique# RelStr

for C being Clique of R

for S being Subset of R st card C = clique# R & C c= S holds

clique# (subrelstr S) = clique# R

for C being Clique of R

for S being Subset of R st card C = clique# R & C c= S holds

clique# (subrelstr S) = clique# R

proof end;

theorem Th44: :: DILWORTH:44

for R being with_finite_stability# RelStr

for S being Subset of R holds stability# (subrelstr S) <= stability# R

for S being Subset of R holds stability# (subrelstr S) <= stability# R

proof end;

theorem Th45: :: DILWORTH:45

for R being with_finite_stability# RelStr

for A being StableSet of R

for S being Subset of R st card A = stability# R & A c= S holds

stability# (subrelstr S) = stability# R

for A being StableSet of R

for S being Subset of R st card A = stability# R & A c= S holds

stability# (subrelstr S) = stability# R

proof end;

definition

let R be RelStr ;

let P be a_partition of the carrier of R;

end;
let P be a_partition of the carrier of R;

attr P is Clique-wise means :Def11: :: DILWORTH:def 11

for x being set st x in P holds

x is Clique of R;

for x being set st x in P holds

x is Clique of R;

:: deftheorem Def11 defines Clique-wise DILWORTH:def 11 :

for R being RelStr

for P being a_partition of the carrier of R holds

( P is Clique-wise iff for x being set st x in P holds

x is Clique of R );

for R being RelStr

for P being a_partition of the carrier of R holds

( P is Clique-wise iff for x being set st x in P holds

x is Clique of R );

registration

let R be RelStr ;

existence

ex b_{1} being a_partition of the carrier of R st b_{1} is Clique-wise

end;
existence

ex b

proof end;

definition
end;

registration

let R be empty RelStr ;

coherence

for b_{1} being a_partition of the carrier of R st b_{1} is empty holds

b_{1} is Clique-wise
;

end;
coherence

for b

b

theorem Th47: :: DILWORTH:47

for R being with_finite_stability# RelStr

for A being StableSet of R

for C being Clique-partition of R st card C = card A holds

ex f being Function of A,C st

( f is bijective & ( for x being set st x in A holds

x in f . x ) )

for A being StableSet of R

for C being Clique-partition of R st card C = card A holds

ex f being Function of A,C st

( f is bijective & ( for x being set st x in A holds

x in f . x ) )

proof end;

theorem Th48: :: DILWORTH:48

for R being finite RelStr

for A being StableSet of R

for C being Clique-partition of R st card C = card A holds

for c being set st c in C holds

ex a being Element of A st c /\ A = {a}

for A being StableSet of R

for C being Clique-partition of R st card C = card A holds

for c being set st c in C holds

ex a being Element of A st c /\ A = {a}

proof end;

theorem Th49: :: DILWORTH:49

for R being non empty transitive antisymmetric with_finite_stability# RelStr

for A being StableSet of R

for U being Clique-partition of (subrelstr (Upper A))

for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds

ex C being Clique-partition of R st card C = stability# R

for A being StableSet of R

for U being Clique-partition of (subrelstr (Upper A))

for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds

ex C being Clique-partition of R st card C = stability# R

proof end;

definition

let R be RelStr ;

let P be a_partition of the carrier of R;

end;
let P be a_partition of the carrier of R;

attr P is StableSet-wise means :Def12: :: DILWORTH:def 12

for x being set st x in P holds

x is StableSet of R;

for x being set st x in P holds

x is StableSet of R;

:: deftheorem Def12 defines StableSet-wise DILWORTH:def 12 :

for R being RelStr

for P being a_partition of the carrier of R holds

( P is StableSet-wise iff for x being set st x in P holds

x is StableSet of R );

for R being RelStr

for P being a_partition of the carrier of R holds

( P is StableSet-wise iff for x being set st x in P holds

x is StableSet of R );

registration

let R be RelStr ;

existence

ex b_{1} being a_partition of the carrier of R st b_{1} is StableSet-wise

end;
existence

ex b

proof end;

definition
end;

registration

let R be empty RelStr ;

coherence

for b_{1} being a_partition of the carrier of R holds b_{1} is StableSet-wise
;

end;
coherence

for b

:: There seems to be little theory of antisymmetric transitive relations.

:: Posets are required to be reflexive and antisymmetric while

:: strict posets to be irreflexive and asymmetric (and both are

:: required to be transitive.) Since asymmetric implies antisymmetric,

:: it seems that the common ground would be antisymmetric and transitive

:: relations.

:: Dilworth's Decomposition Theorem

:: Posets are required to be reflexive and antisymmetric while

:: strict posets to be irreflexive and asymmetric (and both are

:: required to be transitive.) Since asymmetric implies antisymmetric,

:: it seems that the common ground would be antisymmetric and transitive

:: relations.

:: Dilworth's Decomposition Theorem

theorem Th51: :: DILWORTH:51

for R being finite transitive antisymmetric RelStr ex C being Clique-partition of R st card C = stability# R

proof end;

:: deftheorem defines strong-chain DILWORTH:def 13 :

for R being non empty with_finite_stability# RelStr

for C being Subset of R holds

( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st

( card P <= stability# R & ex c being set st

( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds

C /\ d = {} ) ) ) );

for R being non empty with_finite_stability# RelStr

for C being Subset of R holds

( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st

( card P <= stability# R & ex c being set st

( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds

C /\ d = {} ) ) ) );

registration

let R be non empty with_finite_stability# RelStr ;

coherence

for b_{1} being Subset of R st b_{1} is strong-chain holds

b_{1} is clique

end;
coherence

for b

b

proof end;

registration

let R be non empty transitive antisymmetric with_finite_stability# RelStr ;

coherence

for b_{1} being Subset of R st b_{1} is 1 -element holds

b_{1} is strong-chain

end;
coherence

for b

b

proof end;

theorem Th52: :: DILWORTH:52

for R being non empty transitive antisymmetric with_finite_stability# RelStr ex S being non empty Subset of R st

( S is strong-chain & ( for D being Subset of R holds

( not D is strong-chain or not S c< D ) ) )

( S is strong-chain & ( for D being Subset of R holds

( not D is strong-chain or not S c< D ) ) )

proof end;

theorem :: DILWORTH:53

for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R

proof end;

theorem :: DILWORTH:54

for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R

proof end;

theorem Th55: :: DILWORTH:55

for R being finite transitive antisymmetric RelStr

for r, s being Nat holds

( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )

for r, s being Nat holds

( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )

proof end;

:: In a sequence of n^2+1 (distinct) real numbers there is a monotone

:: subsequence of length at least n+1.

:: Let F be the sequence. Define a RelStr with the carrier equal F (a set

:: of ordered pairs) and the relation defined as: if a = [i,F.i] in F and

:: b = [j,F.j] in F, for some i and j, then a < b iff i < j & F.i < F.j.

:: The relation is asymmetric and transitive.

:: Considered defining FinSubsequence of f but have given up.

:: There is not much gain from having FinSubsequence of f instead of

:: FinSubsequence st g c= f

:: subsequence of length at least n+1.

:: Let F be the sequence. Define a RelStr with the carrier equal F (a set

:: of ordered pairs) and the relation defined as: if a = [i,F.i] in F and

:: b = [j,F.j] in F, for some i and j, then a < b iff i < j & F.i < F.j.

:: The relation is asymmetric and transitive.

:: Considered defining FinSubsequence of f but have given up.

:: There is not much gain from having FinSubsequence of f instead of

:: FinSubsequence st g c= f

theorem :: DILWORTH:56

for f being real-valued FinSequence

for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds

ex g being real-valued FinSubsequence st

( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )

for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds

ex g being real-valued FinSubsequence st

( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )

proof end;