:: The Well Ordering Relations
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-2017 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;