The abstract of the Mizar article:

Fixpoints in Complete Lattices

by

Piotr Rudnicki, and

Andrzej Trybulec

Received September 16, 1996

MML identifier: KNASTER

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCT_4, COHSP_1, FUNCOP_1, SETFAM_1,
      TARSKI, SGRAPH1, CARD_1, LATTICES, BINOP_1, ORDINAL1, ORDINAL2, LATTICE3,
      FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1, BHSP_3, SEQM_3, KNASTER,
      PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, RELAT_2,
      RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1,
      SETFAM_1, FUNCT_4, WELLORD1, ORDINAL1, ORDINAL2, CARD_1, COHSP_1,
      LATTICES, LATTICE3, QUANTAL1, ORDERS_1, FUNCT_7;
 constructors NAT_1, BINOP_1, DOMAIN_1, WELLORD2, COHSP_1, BOOLEALG, QUANTAL1,
      PROB_1, FUNCT_7, WELLORD1;
 clusters SUBSET_1, STRUCT_0, FUNCT_1, LATTICES, CARD_1, LATTICE3, RELSET_1,
      ORDINAL1, QUANTAL1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

reserve f, g, h for Function;

theorem :: KNASTER:1
 f is one-to-one & g is one-to-one & rng f misses rng g
  implies f+*g is one-to-one;

canceled;

theorem :: KNASTER:3
   h = f \/ g & dom f misses dom g implies
  (h is one-to-one iff f is one-to-one & g is one-to-one & rng f misses rng g);

begin :: Fix points in general

definition
  let x be set, f be Function;
 pred x is_a_fixpoint_of f means
:: KNASTER:def 1
 x in dom f & x = f.x;
end;

definition
  let A be non empty set, a be Element of A, f be Function of A, A;
 redefine pred a is_a_fixpoint_of f means
:: KNASTER:def 2
 a = f.a;
end;

 reserve x, y, z, u, X for set,
         A for non empty set,
         n for Nat,
         f for Function of X, X;

theorem :: KNASTER:4
 x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f,n);

theorem :: KNASTER:5
   (ex n st x is_a_fixpoint_of iter(f,n) &
          for y st y is_a_fixpoint_of iter(f,n) holds x = y)
 implies x is_a_fixpoint_of f;

definition let A, B be non empty set, f be Function of A, B;
 redefine attr f is c=-monotone means
:: KNASTER:def 3
 for x, y being Element of A st x c= y holds f.x c= f.y;
end;

definition let A be set, B be non empty set;
 cluster c=-monotone Function of A, B;
end;

definition let X be set;
            let f be c=-monotone Function of bool X, bool X;
 func lfp (X, f) -> Subset of X equals
:: KNASTER:def 4
  meet {h where h is Subset of X : f.h c= h};
 func gfp (X, f) -> Subset of X equals
:: KNASTER:def 5
  union {h where h is Subset of X : h c= f.h };
end;

reserve f for c=-monotone Function of bool X, bool X,
        S for Subset of X;

theorem :: KNASTER:6
 lfp(X, f) is_a_fixpoint_of f;

theorem :: KNASTER:7
  gfp(X, f) is_a_fixpoint_of f;

theorem :: KNASTER:8
 f.S c= S implies lfp(X,f) c= S;

theorem :: KNASTER:9
  S c= f.S implies S c= gfp(X,f);

theorem :: KNASTER:10
 S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f);

scheme Knaster{A() -> set, F(set) -> set}:
 ex D being set st F(D) = D & D c= A()
provided
 for X, Y being set st X c= Y holds F(X) c= F(Y) and
 F(A()) c= A();

reserve X, Y for non empty set,
        f for Function of X, Y,
        g for Function of Y, X;

theorem :: KNASTER:11  :: Banach decomposition
  ex Xa, Xb, Ya, Yb being set st
   Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y &
   f.:Xa = Ya & g.:Yb = Xb;

theorem :: KNASTER:12  :: Schroeder-Bernstein
 f is one-to-one & g is one-to-one implies
   ex h being Function of X,Y st h is bijective;

theorem :: KNASTER:13
 (ex f st f is bijective) implies X,Y are_equipotent;

theorem :: KNASTER:14
   f is one-to-one & g is one-to-one implies X,Y are_equipotent;

begin :: The lattice of a lattice subset

definition
  let L be non empty LattStr, f be UnOp of L, x be Element of L;
 redefine func f.x -> Element of L;
end;

definition
 let L be Lattice, f be Function of the carrier of L, the carrier of L,
     x be Element of L, O be Ordinal;
 func (f, O)+.x means
:: KNASTER:def 6
 ex L0 being T-Sequence st it = last L0 & dom L0 = succ O & L0.{} = x &
     (for C being Ordinal st succ C in succ O holds L0.succ C = f.(L0.C)) &
      for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
             holds L0.C = "\/"(rng(L0|C), L);
 func (f, O)-.x means
:: KNASTER:def 7
 ex L0 being T-Sequence st it = last L0 & dom L0 = succ O & L0.{} = x &
     (for C being Ordinal st succ C in succ O holds L0.succ C = f.(L0.C)) &
      for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
             holds L0.C = "/\"(rng(L0|C) , L);
end;

reserve L for Lattice,
        f for Function of the carrier of L, the carrier of L,
          x for Element of L,
        O, O1, O2, O3, O4 for Ordinal,
        T for T-Sequence;

canceled;

theorem :: KNASTER:16
 (f, {})+.x = x;

theorem :: KNASTER:17
 (f, {})-.x = x;

theorem :: KNASTER:18
 (f, succ O)+.x = f.(f, O)+.x;

theorem :: KNASTER:19
 (f, succ O)-.x = f.(f, O)-.x;

theorem :: KNASTER:20
  O <> {} & O is_limit_ordinal & dom T = O &
  (for A being Ordinal st A in O holds T.A = (f, A)+.x)
 implies (f, O)+.x = "\/"(rng T, L);

theorem :: KNASTER:21
  O <> {} & O is_limit_ordinal & dom T = O &
  (for A being Ordinal st A in O holds T.A = (f, A)-.x)
 implies (f, O)-.x = "/\"(rng T, L);

theorem :: KNASTER:22
    iter(f, n).x = (f, n)+.x;

theorem :: KNASTER:23
   iter(f, n).x = (f, n)-.x;


definition
 let L be Lattice, f be (UnOp of the carrier of L),
     a be Element of L, O be Ordinal;
 redefine func (f, O)+.a -> Element of L;
end;

definition
 let L be Lattice, f be (UnOp of the carrier of L),
     a be Element of L, O be Ordinal;
 redefine func (f, O)-.a -> Element of L;
end;

definition
 let L be non empty LattStr, P be Subset of L;
 attr P is with_suprema means
:: KNASTER:def 8

  for x,y being Element of L st x in P & y in P
   ex z being Element of L st z in P & x [= z & y [= z &
    for z' being Element of L st z' in P & x [= z' & y [= z' holds z [= z';
 attr P is with_infima means
:: KNASTER:def 9

  for x,y being Element of L st x in P & y in P
   ex z being Element of L st z in P & z [= x & z [= y &
    for z' being Element of L st z' in P & z' [= x & z' [= y holds z' [= z;
end;

definition
 let L be Lattice;
 cluster non empty with_suprema with_infima Subset of L;
end;

definition
 let L be Lattice,
     P be non empty with_suprema with_infima Subset of L;
func latt P -> strict Lattice means
:: KNASTER:def 10

  the carrier of it = P &
  for x, y being Element of it ex x', y' being Element of L st x = x' & y = y'
          & (x [= y iff x' [= y');
end;

begin :: Complete lattices ::::::::::::::::::::::::::::::::::::::::::::::::

definition
cluster complete -> bounded Lattice;
end;

reserve L for complete Lattice,
        f for (monotone UnOp of L),
        a, b for Element of L;

theorem :: KNASTER:24
 ex a st a is_a_fixpoint_of f;

theorem :: KNASTER:25
 for a st a [= f.a for O holds a [= (f, O)+.a;

theorem :: KNASTER:26
 for a st f.a [= a for O holds (f, O)-.a [= a;

theorem :: KNASTER:27
  for a st a [= f.a
   for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a;

theorem :: KNASTER:28
  for a st f.a [= a
   for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a;

theorem :: KNASTER:29
  for a st a [= f.a
   for O1, O2 st O1 c< O2 & not (f, O2)+.a is_a_fixpoint_of f
    holds (f, O1)+.a <> (f, O2)+.a;

theorem :: KNASTER:30
  for a st f.a [= a
   for O1, O2 st O1 c< O2 & not (f, O2)-.a is_a_fixpoint_of f
    holds (f, O1)-.a <> (f, O2)-.a;

theorem :: KNASTER:31
 a [= f.a & (f, O1)+.a is_a_fixpoint_of f implies
  for O2 st O1 c= O2 holds (f, O1)+.a = (f, O2)+.a;

theorem :: KNASTER:32
 f.a [= a & (f, O1)-.a is_a_fixpoint_of f implies
  for O2 st O1 c= O2 holds (f, O1)-.a = (f, O2)-.a;

theorem :: KNASTER:33
  for a st a [= f.a
   ex O st Card O <=` Card the carrier of L & (f, O)+.a is_a_fixpoint_of f;

theorem :: KNASTER:34
  for a st f.a [= a
   ex O st Card O <=` Card the carrier of L & (f, O)-.a is_a_fixpoint_of f;

theorem :: KNASTER:35
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f
   ex O st Card O <=` Card the carrier of L &
      (f, O)+.(a"\/"b) is_a_fixpoint_of f &
      a [= (f, O)+.(a"\/"b) & b [= (f, O)+.(a"\/"b);

theorem :: KNASTER:36
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f
   ex O st Card O <=` Card the carrier of L &
      (f, O)-.(a"/\"b) is_a_fixpoint_of f &
      (f, O)-.(a"/\"b) [= a & (f, O)-.(a"/\"b) [= b;

theorem :: KNASTER:37
 a [= f.a & a [= b & b is_a_fixpoint_of f
  implies for O2 holds (f, O2)+.a [= b;

theorem :: KNASTER:38
 f.a [= a & b [= a & b is_a_fixpoint_of f
  implies for O2 holds b [= (f, O2)-.a;

definition
 let L be complete Lattice, f be UnOp of L such that
 f is monotone;
 func FixPoints f -> strict Lattice means
:: KNASTER:def 11

 ex P being non empty with_suprema with_infima Subset of L st
    P = {x where x is Element of L: x is_a_fixpoint_of f} &
    it = latt P;
end;

theorem :: KNASTER:39
 the carrier of FixPoints f = {x where x is Element of L: x is_a_fixpoint_of f}
;

theorem :: KNASTER:40
  the carrier of FixPoints f c= the carrier of L;

theorem :: KNASTER:41
  (a in the carrier of FixPoints f iff a is_a_fixpoint_of f);

theorem :: KNASTER:42
  for x, y being Element of FixPoints f, a, b
     st x = a & y = b holds (x [= y iff a [= b);

theorem :: KNASTER:43
    FixPoints f is complete;

definition
 let L, f;
 func lfp f -> Element of L equals
:: KNASTER:def 12
  (f, nextcard the carrier of L)+.Bottom L;
 func gfp f -> Element of L equals
:: KNASTER:def 13
  (f, nextcard the carrier of L)-.Top L;
end;

theorem :: KNASTER:44
 (lfp f is_a_fixpoint_of f) &
 (ex O st Card O <=` Card the carrier of L & (f, O)+.Bottom L = lfp f);

theorem :: KNASTER:45
 (gfp f is_a_fixpoint_of f) &
 (ex O st Card O <=` Card the carrier of L & (f, O)-.Top L = gfp f);

theorem :: KNASTER:46
  a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f;


theorem :: KNASTER:47
   f.a [= a implies lfp f [= a;

theorem :: KNASTER:48
   a [= f.a implies a [= gfp f;

begin :: Boolean Lattices

reserve f for (monotone UnOp of BooleLatt A);

definition
 let A be set;
 cluster BooleLatt A -> complete;
end;

theorem :: KNASTER:49
 for f being UnOp of BooleLatt A
  holds f is monotone iff f is c=-monotone;

theorem :: KNASTER:50
    ex g being c=-monotone Function of bool A, bool A st lfp (A, g) = lfp f;

theorem :: KNASTER:51
    ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f;