:: On the Isomorphism Between Finite Chains :: by Marta Pruszy\'nska and Marek Dudzicz :: :: Received June 29, 2000 :: Copyright (c) 2000-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TREES_2, ORDERS_2, RELAT_2, XBOOLE_0, STRUCT_0, ZFMISC_1, CARD_3, FINSET_1, CAT_1, YELLOW_0, SUBSET_1, XXREAL_0, TARSKI, NAT_1, YELLOW_1, WELLORD2, WELLORD1, ARYTM_3, LATTICES, FUNCT_1, FUNCT_4, RELAT_1, CARD_1, FUNCOP_1, ARYTM_1, PBOOLE, ORDERS_4; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, PBOOLE, CARD_3, RELAT_2, ORDERS_1, ORDERS_2, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_4, DOMAIN_1, STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WELLORD1, XXREAL_0; constructors DOMAIN_1, NAT_1, NAT_D, MEMBERED, TOLER_1, LATTICE3, ORDERS_3, WAYBEL_1, RELSET_1, CARD_3; registrations XBOOLE_0, RELSET_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, YELLOW11, CARD_1, ORDERS_2; 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; registration cluster empty -> reflexive transitive antisymmetric for RelStr; end; registration cluster -> reflexive transitive antisymmetric for Chain; end; registration cluster non empty for Chain; end; registration cluster -> connected for 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; registration cluster finite non empty for Chain; end; registration cluster countable for Chain; end; registration let A be connected non empty RelStr; cluster full -> connected for non empty SubRelStr of A; end; registration let A be finite RelStr; cluster -> finite for 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 Function 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 Function of subrelstr A1, subrelstr A2 st f is isomorphic for g be Function of subrelstr B1, subrelstr B2 st g is isomorphic ex h be Function 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;