The abstract of the Mizar article:

On the Isomorphism between Finite Chains

by

Marta Pruszynska, and

Marek Dudzicz

Received June 29, 2000

MML identifier: ORDERS_4

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, RELAT_2, REALSET1, CARD_4, FINSET_1, CAT_1, YELLOW_0,
      YELLOW_1, WELLORD2, WELLORD1, BOOLE, LATTICES, PRE_TOPC, FUNCT_4,
      RELAT_1, FUNCT_1, ORDINAL1, CARD_1, FUNCOP_1, ARYTM_1, PBOOLE, ORDERS_4;
 notation TARSKI, XBOOLE_0, STRUCT_0, XCMPLX_0, XREAL_0, FINSET_1, NAT_1,
      FUNCOP_1, GROUP_1, PBOOLE, CARD_1, CARD_4, REALSET1, RELAT_2, ORDERS_1,
      PRE_TOPC, RELAT_1, FUNCT_1, FUNCT_2, YELLOW_0, WAYBEL_0, YELLOW_1,
      WAYBEL_1, FUNCT_4, WELLORD1, ORDINAL1;
 constructors CARD_4, WAYBEL_1, NAT_1, REAL_1, ORDERS_3, GROUP_6, WAYBEL_8,
      WAYBEL19, WAYBEL23, MEMBERED, TOLER_1;
 clusters FINSET_1, WAYBEL_0, STRUCT_0, YELLOW_0, YELLOW_1, WAYBEL_2, XREAL_0,
      YELLOW13, RELSET_1, WAYBEL31, FUNCOP_1, YELLOW14, YELLOW_2, NAT_1,
      MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

definition
 mode Chain -> RelStr means
:: ORDERS_4:def 1
  it is connected (non empty Poset) or it is empty;
end;

definition
 cluster empty -> reflexive transitive antisymmetric RelStr;
end;

definition
 cluster -> reflexive transitive antisymmetric Chain;
end;

definition
 cluster non empty Chain;
end;

definition
 cluster -> connected (non empty Chain);
end;

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

definition
  cluster finite non empty Chain;
end;

definition
  cluster countable Chain;
end;

definition let A be connected (non empty RelStr);
  cluster full -> connected (non empty SubRelStr of A);
end;

definition let A be finite RelStr;
  cluster -> finite SubRelStr of A;
end;

theorem :: ORDERS_4:1
for n,m be Nat holds
 n <= m implies InclPoset(n) is full SubRelStr of InclPoset(m);

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

theorem :: ORDERS_4:2
 for L be RelStr
  for A,B be set holds
   A,B form_upper_lower_partition_of L implies A misses B;

theorem :: ORDERS_4:3
for L be upper-bounded antisymmetric non empty RelStr holds
 ((the carrier of L) \ { Top L }), { Top L } form_upper_lower_partition_of L;

theorem :: ORDERS_4:4
for L1,L2 be RelStr
 for f be map of L1,L2 st f is isomorphic
  holds (the carrier of L1 <> {} iff the carrier of L2 <> {})
   & (the carrier of L2 <> {} or the carrier of L1 = {})
    & (the carrier of L1 = {} iff the carrier of L2 = {});

theorem :: ORDERS_4:5
for L1,L2 be antisymmetric RelStr
 for A1,B1 be Subset of L1 st A1,B1 form_upper_lower_partition_of L1
  for A2,B2 be Subset of L2 st A2,B2 form_upper_lower_partition_of L2
   for f be map of subrelstr A1, subrelstr A2 st f is isomorphic
    for g be map of subrelstr B1, subrelstr B2 st g is isomorphic
     ex h be map of L1,L2 st h = f +* g & h is isomorphic;

theorem :: ORDERS_4:6
  for A being finite Chain, n being Nat st Card(the carrier of A) = n holds
    A,InclPoset n are_isomorphic;