:: On the Isomorphism Between Finite Chains
:: by Marta Pruszy\'nska and Marek Dudzicz
::
:: Received June 29, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

definition

mode Chain -> RelStr means :Def1: :: ORDERS_4:def 1
( it is non empty connected Poset or it is empty );
existence
ex b₁ being RelStr st
( b₁ is non empty connected Poset or b₁ is empty )

proof end;

end;

:: deftheorem Def1 defines Chain ORDERS_4:def 1 :
for b₁ being RelStr holds
( b₁ is Chain iff ( b₁ is non empty connected Poset or b₁ is empty ) );

registration

cluster empty -> reflexive transitive antisymmetric RelStr ;
coherence
for b₁ being RelStr st b₁ is empty holds
( b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric )

proof end;

end;

registration

cluster -> reflexive transitive antisymmetric Chain ;
coherence
for b₁ being Chain holds
( b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric )

proof end;

end;

registration

cluster non empty V73() reflexive transitive antisymmetric Chain ;
existence
not for b₁ being Chain holds b₁ is empty

proof end;

end;

registration

cluster non empty -> non empty connected Chain ;
coherence
for b₁ being non empty Chain holds b₁ is connected by Def1;

end;

definition

let L be 1-sorted ;
attr L is countable means :Def2: :: ORDERS_4:def 2
the carrier of L is countable ;

end;

:: deftheorem Def2 defines countable ORDERS_4:def 2 :
for L being 1-sorted holds
( L is countable iff the carrier of L is countable );

registration

cluster non empty finite V73() reflexive transitive antisymmetric Chain ;
existence
ex b₁ being Chain st
( b₁ is finite & not b₁ is empty )

proof end;

end;

registration

cluster V73() reflexive transitive antisymmetric countable Chain ;
existence
ex b₁ being Chain st b₁ is countable

proof end;

end;

registration

let A be non empty connected RelStr ;
cluster non empty full -> non empty connected SubRelStr of A;
correctness
coherence
for b₁ being non empty SubRelStr of A st b₁ is full holds
b₁ is connected ;

proof end;

end;

registration

let A be finite RelStr ;
cluster -> finite SubRelStr of A;
correctness
coherence
for b₁ being SubRelStr of A holds b₁ is finite ;

proof end;

end;

theorem Th1: :: ORDERS_4:1

for n, m being Nat st n <= m holds
InclPoset n is full SubRelStr of InclPoset m

proof end;

definition

let L be RelStr ;
let A, B be set ;
pred A,B form_upper_lower_partition_of L means :Def3: :: ORDERS_4:def 3
( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) );

end;

:: deftheorem Def3 defines form_upper_lower_partition_of ORDERS_4:def 3 :
for L being RelStr
for A, B being set holds
( A,B form_upper_lower_partition_of L iff ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) ) );

theorem Th2: :: ORDERS_4:2

for L being RelStr
for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B

proof end;

theorem Th3: :: ORDERS_4:3

for L being non empty antisymmetric upper-bounded RelStr holds the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L

proof end;

theorem Th4: :: ORDERS_4:4

for L1, L2 being RelStr
for f being Function of L1,L2 st f is isomorphic holds
( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )

proof end;

theorem Th5: :: ORDERS_4:5

for L1, L2 being antisymmetric RelStr
for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds
for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )

proof end;

theorem :: ORDERS_4:6

for A being finite Chain
for n being Nat st card the carrier of A = n holds
A, InclPoset n are_isomorphic

proof end;