:: The Well Ordering Relations :: by Grzegorz Bancerek :: :: Received April 4, 1989 :: Copyright (c) 1990-2018 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 RELAT_1, RELAT_2, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, ZFMISC_1, WELLORD1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1; constructors TARSKI, SUBSET_1, FUNCT_1, RELAT_2, XTUPLE_0; registrations FUNCT_1, RELAT_1; requirements SUBSET, BOOLE; begin reserve a,b,c,d,x,y,z for object, X,Y,Z for set; reserve R,S,T for Relation; definition let R; let a be object; func R-Seg(a) -> set equals :: WELLORD1:def 1 Coim(R,a) \ {a}; end; theorem :: WELLORD1:1 x in R-Seg a iff x <> a & [x,a] in R; theorem :: WELLORD1:2 x in field R or R-Seg(x) = {}; definition let R; attr R is well_founded means :: WELLORD1:def 2 for Y st Y c= field R & Y <> {} ex a st a in Y & R-Seg a misses Y; let X; pred R is_well_founded_in X means :: WELLORD1:def 3 for Y st Y c= X & Y <> {} ex a st a in Y & R-Seg a misses Y; end; theorem :: WELLORD1:3 R is well_founded iff R is_well_founded_in field R; definition let R; attr R is well-ordering means :: WELLORD1:def 4 R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded; let X; pred R well_orders X means :: WELLORD1:def 5 R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X; end; registration cluster well-ordering -> reflexive transitive antisymmetric connected well_founded for Relation; cluster reflexive transitive antisymmetric connected well_founded -> well-ordering for Relation; end; theorem :: WELLORD1:4 R well_orders field R iff R is well-ordering; theorem :: WELLORD1:5 R well_orders X implies for Y st Y c= X & Y <> {} ex a st a in Y & for b st b in Y holds [a,b] in R; theorem :: WELLORD1:6 R is well-ordering implies for Y st Y c= field R & Y <> {} ex a st a in Y & for b st b in Y holds [a,b] in R; theorem :: WELLORD1:7 for R st R is well-ordering & field R <> {} ex a st a in field R & for b st b in field R holds [a,b] in R; theorem :: WELLORD1:8 for R st R is well-ordering for a st a in field R holds (for b st b in field R holds [b,a] in R) or ex b st b in field R & [a,b] in R & for c st c in field R & [a,c] in R holds c = a or [b,c] in R; reserve F,G for Function; theorem :: WELLORD1:9 R-Seg(a) c= field R; definition let R,Y; func R |_2 Y -> Relation equals :: WELLORD1:def 6 R /\ [:Y,Y:]; end; theorem :: WELLORD1:10 R |_2 X = X|`R|X; theorem :: WELLORD1:11 R |_2 X = X|`(R|X); theorem :: WELLORD1:12 x in field(R |_2 X) implies x in field R & x in X; theorem :: WELLORD1:13 field(R |_2 X) c= field R & field(R |_2 X) c= X; theorem :: WELLORD1:14 (R |_2 X)-Seg(a) c= R-Seg(a); theorem :: WELLORD1:15 R is reflexive implies R |_2 X is reflexive; theorem :: WELLORD1:16 R is connected implies R |_2 Y is connected; theorem :: WELLORD1:17 R is transitive implies R |_2 Y is transitive; theorem :: WELLORD1:18 R is antisymmetric implies R |_2 Y is antisymmetric; theorem :: WELLORD1:19 (R |_2 X) |_2 Y = R |_2 (X /\ Y); theorem :: WELLORD1:20 (R |_2 X) |_2 Y = (R |_2 Y) |_2 X; theorem :: WELLORD1:21 (R |_2 Y) |_2 Y = R |_2 Y; theorem :: WELLORD1:22 Z c= Y implies (R |_2 Y) |_2 Z = R |_2 Z; theorem :: WELLORD1:23 R |_2 field R = R; theorem :: WELLORD1:24 R is well_founded implies R |_2 X is well_founded; theorem :: WELLORD1:25 R is well-ordering implies R |_2 Y is well-ordering; theorem :: WELLORD1:26 R is well-ordering implies R-Seg(a),R-Seg(b) are_c=-comparable; theorem :: WELLORD1:27 R is well-ordering & b in R-Seg(a) implies (R |_2 (R-Seg(a))) -Seg(b) = R-Seg(b); theorem :: WELLORD1:28 R is well-ordering & Y c= field R implies (Y = field R or (ex a st a in field R & Y = R-Seg(a) ) iff for a st a in Y for b st [b,a] in R holds b in Y ); theorem :: WELLORD1:29 R is well-ordering & a in field R & b in field R implies ( [a,b] in R iff R-Seg(a) c= R-Seg(b) ); theorem :: WELLORD1:30 R is well-ordering & a in field R & b in field R implies ( R-Seg (a) c= R-Seg(b) iff a = b or a in R-Seg(b) ); theorem :: WELLORD1:31 R is well-ordering & X c= field R implies field(R |_2 X) = X; theorem :: WELLORD1:32 R is well-ordering implies field(R |_2 R-Seg(a)) = R-Seg(a); theorem :: WELLORD1:33 R is well-ordering implies for Z st for a st a in field R & R -Seg(a) c= Z holds a in Z holds field R c= Z; theorem :: WELLORD1:34 R is well-ordering & a in field R & b in field R & (for c st c in R-Seg(a) holds [c,b] in R & c <> b) implies [a,b] in R; theorem :: WELLORD1:35 R is well-ordering & dom F = field R & rng F c= field R & (for a ,b st [a,b] in R & a <> b holds [F.a,F.b] in R & F.a <> F.b) implies for a st a in field R holds [a,F.a] in R; definition let R,S,F; pred F is_isomorphism_of R,S means :: WELLORD1:def 7 dom F = field R & rng F = field S & F is one-to-one & for a,b holds [a,b] in R iff a in field R & b in field R & [F.a,F.b] in S; end; theorem :: WELLORD1:36 F is_isomorphism_of R,S implies for a,b st [a,b] in R & a <> b holds [F.a,F.b] in S & F.a <> F.b; definition let R,S; pred R,S are_isomorphic means :: WELLORD1:def 8 ex F st F is_isomorphism_of R,S; end; theorem :: WELLORD1:37 id(field R) is_isomorphism_of R,R; theorem :: WELLORD1:38 R,R are_isomorphic; theorem :: WELLORD1:39 F is_isomorphism_of R,S implies F" is_isomorphism_of S,R; theorem :: WELLORD1:40 R,S are_isomorphic implies S,R are_isomorphic; theorem :: WELLORD1:41 F is_isomorphism_of R,S & G is_isomorphism_of S,T implies G*F is_isomorphism_of R,T; theorem :: WELLORD1:42 R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic; theorem :: WELLORD1:43 F is_isomorphism_of R,S implies ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ); theorem :: WELLORD1:44 R is well-ordering & F is_isomorphism_of R,S implies S is well-ordering; theorem :: WELLORD1:45 R is well-ordering implies for F,G st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds F = G; definition let R,S; assume that R is well-ordering and R,S are_isomorphic; func canonical_isomorphism_of(R,S) -> Function means :: WELLORD1:def 9 it is_isomorphism_of R,S; end; theorem :: WELLORD1:46 R is well-ordering implies for a st a in field R holds not R,R |_2 (R-Seg(a)) are_isomorphic; theorem :: WELLORD1:47 R is well-ordering & a in field R & b in field R & a <> b implies not R |_2 (R-Seg(a)),R |_2 (R-Seg(b)) are_isomorphic; theorem :: WELLORD1:48 R is well-ordering & Z c= field R & F is_isomorphism_of R,S implies F|Z is_isomorphism_of R |_2 Z,S |_2 (F.:Z) & R |_2 Z,S |_2 (F.:Z) are_isomorphic; theorem :: WELLORD1:49 F is_isomorphism_of R,S implies for a st a in field R ex b st b in field S & F.:(R-Seg(a)) = S-Seg(b); theorem :: WELLORD1:50 R is well-ordering & F is_isomorphism_of R,S implies for a st a in field R ex b st b in field S & R |_2 (R-Seg(a)),S |_2 (S-Seg(b)) are_isomorphic; theorem :: WELLORD1:51 R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S-Seg(b)) are_isomorphic & R |_2 (R-Seg(a)),S |_2 (S-Seg(c)) are_isomorphic implies S-Seg(c) c= S-Seg(b) & [c,b] in S; theorem :: WELLORD1:52 R is well-ordering & S is well-ordering implies R,S are_isomorphic or (ex a st a in field R & R |_2 (R-Seg(a)),S are_isomorphic ) or ex a st a in field S & R,S |_2 (S-Seg(a)) are_isomorphic; theorem :: WELLORD1:53 Y c= field R & R is well-ordering implies R,R |_2 Y are_isomorphic or ex a st a in field R & R |_2 (R-Seg(a)),R |_2 Y are_isomorphic; :: from AMISTD_3, 2010.01.10, A.T. theorem :: WELLORD1:54 R,S are_isomorphic & R is well-ordering implies S is well-ordering;