The abstract of the Mizar article:

Dickson's Lemma

by

Gilbert Lee, and

Piotr Rudnicki

Received March 12, 2002

MML identifier: DICKSON

[ Mizar article, MML identifier index ]

environ

 vocabulary DICKSON, RELAT_1, RELAT_2, FINSET_1, WELLORD1, ORDERS_2, BOOLE,
      WAYBEL20, EQREL_1, ORDERS_1, NORMSP_1, FUNCT_1, SQUARE_1, SETFAM_1,
      CARD_1, NEWTON, SEQM_3, TARSKI, MCART_1, YELLOW_1, PBOOLE, CARD_3,
      PRE_TOPC, CAT_1, RLVECT_2, WAYBEL_3, YELLOW_6, FUNCOP_1, ORDINAL2,
      FUNCT_4, YELLOW_3, WELLFND1, WAYBEL_4, REARRAN1, PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, RELAT_1,
      RELAT_2, DOMAIN_1, RELSET_1, FINSET_1, MCART_1, WELLORD1, ORDERS_1,
      ORDERS_2, FUNCT_1, EQREL_1, WELLFND1, WAYBEL_0, NUMBERS, XREAL_0, NAT_1,
      CARD_1, NORMSP_1, CQC_SIM1, WAYBEL_4, PARTFUN1, FUNCT_2, SEQM_3,
      PSCOMP_1, FRECHET2, BHSP_3, YELLOW_3, WAYBEL_1, PBOOLE, PRE_TOPC,
      PRALG_1, CARD_3, YELLOW_1, CQC_LANG, WAYBEL_3, YELLOW_6, FUNCT_4,
      PRE_CIRC;
 constructors ORDERS_2, WELLFND1, NAT_1, CQC_SIM1, PRE_CIRC, WAYBEL_4,
      PSCOMP_1, FRECHET2, YELLOW_3, WAYBEL_1, INT_1, ORDERS_3, WAYBEL_3,
      DOMAIN_1, BHSP_3, TOLER_1;
 clusters RELSET_1, FINSET_1, SUBSET_1, STRUCT_0, NAT_1, NORMSP_1, RELAT_1,
      CARD_5, SEQM_3, YELLOW_6, WAYBEL12, YELLOW_3, YELLOW_1, FUNCT_1,
      BINARITH, CQC_LANG, BORSUK_3, WAYBEL18, ORDERS_1, FILTER_1, MEMBERED,
      FUNCT_2, PRE_CIRC, PARTFUN1;
 requirements BOOLE, SUBSET, NUMERALS;


begin :: Preliminaries

theorem :: DICKSON:1
for g being Function, x being set st dom g = {x} holds g = x .--> g.x;

theorem :: DICKSON:2
for n being Nat holds n c= n+1;

scheme FinSegRng2{m, n() -> Nat, F(set)->set, P[Nat]}:
  {F(i) where i is Nat : m()<i & i<=n() & P[i]} is finite;

theorem :: DICKSON:3
for X being infinite set ex f being Function of NAT, X st f is one-to-one;

definition
  let R be RelStr, f be sequence of R;
  attr f is ascending means
:: DICKSON:def 1
    for n being Nat
   holds f.(n+1) <> f.n & [f.n, f.(n+1)] in the InternalRel of R;
end;

definition
  let R be RelStr, f be sequence of R;
  attr f is weakly-ascending means
:: DICKSON:def 2
  for n being Nat holds [f.n, f.(n+1)] in the InternalRel of R;
end;

theorem :: DICKSON:4
for R being non empty transitive RelStr, f being sequence of R
 st f is weakly-ascending
  holds for i,j being Nat st i < j holds f.i <= f.j;

theorem :: DICKSON:5
for R being non empty RelStr
 holds R is connected iff
       the InternalRel of R is_strongly_connected_in the carrier of R;

canceled;

theorem :: DICKSON:7
for L being RelStr, Y being set, a being set
 holds ((the InternalRel of L)-Seg(a) misses Y & a in Y) iff
        a is_minimal_wrt Y, the InternalRel of L;

theorem :: DICKSON:8
for L being non empty transitive antisymmetric RelStr,
    x being Element of L, a, N being set
 st a is_minimal_wrt (the InternalRel of L)-Seg(x) /\ N,(the InternalRel of L)
  holds a is_minimal_wrt N, (the InternalRel of L);

begin :: Chapter 4.2

definition let R be RelStr; :: Def 4.19 (ix)
  attr R is quasi_ordered means
:: DICKSON:def 3
       R is reflexive transitive;
end;

definition :: Lemma 4.24.i
   let R be RelStr such that
 R is quasi_ordered;
   func EqRel R -> Equivalence_Relation of the carrier of R equals
:: DICKSON:def 4
        (the InternalRel of R) /\ (the InternalRel of R)~;
end;

theorem :: DICKSON:9
  for R being RelStr, x,y being Element of R
   st R is quasi_ordered holds x in Class(EqRel R, y) iff x <= y & y <= x;

definition :: Lemma 4.24, (the InternalRel of R) / EqRel R
  let R be RelStr;
  func <=E R -> Relation of Class EqRel R means
:: DICKSON:def 5
  for A, B being set holds [A,B] in it iff
    ex a, b being Element of R
      st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
end;

theorem :: DICKSON:10  :: Lemma 4.24.ii
for R being RelStr
 st R is quasi_ordered holds <=E R partially_orders Class(EqRel R);

theorem :: DICKSON:11 ::Lemma 4.24.iii
  for R being non empty RelStr st R is quasi_ordered & R is connected
  holds <=E R linearly_orders Class(EqRel R);

definition :: "strict part" of a relation, p. 155
  let R be Relation;
  func R\~ -> Relation equals
:: DICKSON:def 6
    R \ R~;
end;

definition
  let R be Relation;
  cluster R \~ -> asymmetric;
end;

definition
  let X be set, R be Relation of X;
  redefine func R\~ -> Relation of X;
end;

definition
   let R be RelStr;
   func R\~ -> strict RelStr equals
:: DICKSON:def 7
     RelStr(# the carrier of R, (the InternalRel of R)\~ #);
end;

definition
  let R be non empty RelStr;
  cluster R\~ -> non empty;
end;

definition
  let R be transitive RelStr;
  cluster R\~ -> transitive;
end;

definition
   let R be RelStr;
   cluster R\~ -> antisymmetric;
end;

theorem :: DICKSON:12 ::Exercise 4.27:
  for R being non empty Poset, x being Element of R
 holds Class(EqRel R, x) = {x};

theorem :: DICKSON:13 :: Exercise 4.29.i
  for R being Relation holds R = R\~ iff R is asymmetric;

theorem :: DICKSON:14 :: Exercise 4.29.ii
  for R being Relation st R is transitive holds R\~ is transitive;

theorem :: DICKSON:15 :: Exercise 4.29.iii
  for R being Relation, a, b being set st R is antisymmetric
 holds [a,b] in R\~ iff [a,b] in R & a <> b;

theorem :: DICKSON:16  :: Exercise 4.29 (addition)
for R being RelStr st R is well_founded holds R\~ is well_founded;

theorem :: DICKSON:17  :: Exercise 4.29 (addition)
for R being RelStr
 st R\~ is well_founded & R is antisymmetric holds R is well_founded;

begin :: Chapter 4.3

theorem :: DICKSON:18  :: Def 4.30 (see WAYBEL_4:def 26)
for L being RelStr, N being set, x being Element of L\~
 holds x is_minimal_wrt N, the InternalRel of (L\~) iff (x in N &
        for y being Element of L st y in N & [y,x] in the InternalRel of L
         holds [x,y] in the InternalRel of L);

:: Proposition 4.31 - see WELLFND1:15

:: Omitting Example 4.32, Exercise 4.33, Exercise 4.34

theorem :: DICKSON:19 ::L_4_35: :: Lemma 4.35
  for R, S being non empty RelStr, m being map of R,S
 st R is quasi_ordered & S is antisymmetric & S\~ is well_founded &
    for a,b being Element of R holds
       (a <= b implies m.a <= m.b) & (m.a = m.b implies [a,b] in EqRel R)
  holds R\~ is well_founded;

definition :: p. 158, restricted eq classes
  let R be non empty RelStr, N be Subset of R;
  func min-classes N -> Subset-Family of R means
:: DICKSON:def 8
    for x being set holds x in it iff
      ex y being Element of R\~
       st y is_minimal_wrt N, the InternalRel of (R\~) &
          x = Class(EqRel R,y) /\ N;
end;

theorem :: DICKSON:20  :: Lemma 4.36
for R being non empty RelStr, N being Subset of R, x being set
 st R is quasi_ordered & x in min-classes N
  holds for y being Element of R\~ st y in x
          holds y is_minimal_wrt N, the InternalRel of R\~;

theorem :: DICKSON:21
for R being non empty RelStr
 holds R\~ is well_founded iff
       for N being Subset of R st N <> {}
         ex x being set st x in min-classes N;

theorem :: DICKSON:22
for R being non empty RelStr, N being Subset of R,
    y being Element of R\~
 st y is_minimal_wrt N, the InternalRel of (R\~)
  holds min-classes N is non empty;

theorem :: DICKSON:23
for R being non empty RelStr, N being Subset of R, x being set
  st R is quasi_ordered & x in min-classes N holds x is non empty;

theorem :: DICKSON:24  :: Lemma 4.37
for R being non empty RelStr st R is quasi_ordered
 holds R is connected & R\~ is well_founded iff
       for N being non empty Subset of R
        holds Card min-classes N = 1;

theorem :: DICKSON:25 :: Lemma 4.38
  for R being non empty Poset
 holds the InternalRel of R well_orders the carrier of R iff
       for N being non empty Subset of R
        holds Card min-classes N = 1;

definition :: Def 4.39
  let R be RelStr, N be Subset of R, B be set;
  pred B is_Dickson-basis_of N,R means
:: DICKSON:def 9
       B c= N & for a being Element of R st a in N
                 ex b being Element of R st b in B & b <= a;
end;

theorem :: DICKSON:26
for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R, R;

theorem :: DICKSON:27
for R being non empty RelStr, N being non empty Subset of R,
    B being set
 st B is_Dickson-basis_of N,R holds B is non empty;

definition :: Def 4.39
  let R be RelStr;
  attr R is Dickson means
:: DICKSON:def 10
  for N being Subset of R
   ex B being set st B is_Dickson-basis_of N,R & B is finite;
end;

theorem :: DICKSON:28  :: Lemma 4:40
for R being non empty RelStr
 st R\~ is well_founded & R is connected holds R is Dickson;

theorem :: DICKSON:29  :: Exercise 4.41
for R, S being RelStr st (the InternalRel of R) c= (the InternalRel of S) &
    R is Dickson & (the carrier of R) = (the carrier of S)
  holds S is Dickson;

definition
   let f be Function, b be set such that
 dom f = NAT and
 b in rng f;
   func f mindex b -> Nat means
:: DICKSON:def 11
        f.it = b & for i being Nat st f.i = b holds it <= i;
end;

definition
   let R be non empty 1-sorted, f be sequence of R, b be set, m be Nat; assume
 ex j being Nat st m < j & f.j = b;
   func f mindex (b,m) -> Nat means
:: DICKSON:def 12
        f.it = b & m < it & for i being Nat st m < i & f.i = b holds it <= i;
end;

theorem :: DICKSON:30  :: Prop 4.42 (i) -> (ii)
for R being non empty RelStr st R is quasi_ordered & R is Dickson
 holds for f being sequence of R ex i,j being Nat st i < j & f.i <= f.j;

theorem :: DICKSON:31
for R being RelStr, N being Subset of R, x being Element of R\~
 st R is quasi_ordered & x in N &
    ((the InternalRel of R)-Seg(x)) /\ N c= Class(EqRel R,x)
  holds x is_minimal_wrt N, the InternalRel of R\~;

theorem :: DICKSON:32  :: Prop 4.42 (ii) -> (iii)
for R being non empty RelStr
 st R is quasi_ordered &
    (for f being sequence of R ex i,j being Nat st i < j & f.i <= f.j)
  holds for N being non empty Subset of R
          holds min-classes N is finite & min-classes N is non empty;

theorem :: DICKSON:33  :: Prop (iii) -> (i)
for R being non empty RelStr
  st R is quasi_ordered &
     (for N being non empty Subset of R
       holds min-classes N is finite & min-classes N is non empty)
   holds R is Dickson;

theorem :: DICKSON:34  :: Corollary 4.44
for R being non empty RelStr st R is quasi_ordered & R is Dickson
 holds R\~ is well_founded;

theorem :: DICKSON:35 :: Corollary 4.43
  for R being non empty Poset, N being non empty Subset of R
 st R is Dickson
  holds ex B being set st B is_Dickson-basis_of N, R &
              for C being set st C is_Dickson-basis_of N, R holds B c= C;

definition
  let R be non empty RelStr, N be Subset of R such that
 R is Dickson;
  func Dickson-bases (N,R) -> non empty Subset-Family of R means
:: DICKSON:def 13

    for B being set holds B in it iff B is_Dickson-basis_of N,R;
end;

theorem :: DICKSON:36  :: Proposition 4.45
for R being non empty RelStr, s being sequence of R st R is Dickson
  ex t being sequence of R st t is_subsequence_of s & t is weakly-ascending;

theorem :: DICKSON:37
for R being RelStr st R is empty holds R is Dickson;

theorem :: DICKSON:38   :: Theorem 4.46
for M, N be RelStr
 st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered
  holds [:M,N:] is quasi_ordered & [:M,N:] is Dickson;

theorem :: DICKSON:39
for R, S being RelStr st R,S are_isomorphic & R is Dickson & R is quasi_ordered
 holds S is quasi_ordered & S is Dickson;

theorem :: DICKSON:40
for p being RelStr-yielding ManySortedSet of 1, z being Element of 1
 holds p.z, product p are_isomorphic;

definition
  let X be set, p be RelStr-yielding ManySortedSet of X, Y be Subset of X;
  cluster p|Y -> RelStr-yielding;
end;

theorem :: DICKSON:41
for n being non empty Nat, p being RelStr-yielding ManySortedSet of n
 holds product p is non empty iff p is non-Empty;

theorem :: DICKSON:42
for n being non empty Nat, p being RelStr-yielding ManySortedSet of n+1,
    ns being Subset of n+1, ne being Element of n+1
 st ns = n & ne = n holds [:product (p|ns), p.ne:], product p are_isomorphic;

theorem :: DICKSON:43  :: Corollary 4.47
for n being non empty Nat, p being RelStr-yielding ManySortedSet of n
  st for i being Element of n holds p.i is Dickson & p.i is quasi_ordered
    holds product p is quasi_ordered & product p is Dickson;

definition
 let p be RelStr-yielding ManySortedSet of {};
 cluster product p -> non empty;
 cluster product p -> antisymmetric;
 cluster product p -> quasi_ordered;
 cluster product p -> Dickson;
end;

definition
  func NATOrd -> Relation of NAT equals
:: DICKSON:def 14
    {[x,y] where x, y is Element of NAT : x <= y};
end;

theorem :: DICKSON:44
NATOrd is_reflexive_in NAT;

theorem :: DICKSON:45
NATOrd is_antisymmetric_in NAT;

theorem :: DICKSON:46
NATOrd is_strongly_connected_in NAT;

theorem :: DICKSON:47
NATOrd is_transitive_in NAT;

definition
  func OrderedNAT -> non empty RelStr equals
:: DICKSON:def 15
    RelStr(# NAT, NATOrd #);
end;

definition
  cluster OrderedNAT -> connected;
  cluster OrderedNAT -> Dickson;
  cluster OrderedNAT -> quasi_ordered;
  cluster OrderedNAT -> antisymmetric;
  cluster OrderedNAT -> transitive;
  cluster OrderedNAT -> well_founded;
end;

definition :: 4.48 Dickson's Lemma
 let n be Nat;
 cluster product (n --> OrderedNAT) -> non empty;
 cluster product (n --> OrderedNAT) -> Dickson;
 cluster product (n --> OrderedNAT) -> quasi_ordered;
 cluster product (n --> OrderedNAT) -> antisymmetric;
end;

theorem :: DICKSON:48
 :: Proposition 4.49, in B&W proven without axiom of choice (4.46)
  for M be RelStr
 st M is Dickson & M is quasi_ordered
  holds [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson;

:: Omitting Exercise 4.50

theorem :: DICKSON:49  :: Lemma 4.51
for R, S being non empty RelStr
 st R is Dickson & R is quasi_ordered & S is quasi_ordered &
    the InternalRel of R c= the InternalRel of S &
    (the carrier of R) = (the carrier of S)
  holds S\~ is well_founded;

theorem :: DICKSON:50 :: Lemma 4.52
  for R being non empty RelStr st R is quasi_ordered
 holds R is Dickson iff
       for S being non empty RelStr
        st S is quasi_ordered & the InternalRel of R c= the InternalRel of S &
           the carrier of R = the carrier of S
         holds S\~ is well_founded;