The abstract of the Mizar article:

Abian's Fixed Point Theorem

by

Piotr Rudnicki, and

Andrzej Trybulec

Received February 22, 1997

MML identifier: ABIAN

[ Mizar article, MML identifier index ]

environ

 vocabulary SETFAM_1, FUNCT_1, ARYTM, MATRIX_2, INT_1, ARYTM_1, FUNCT_4,
      TRIANG_1, ZF_REFLE, FUNCOP_1, RELAT_1, SQUARE_1, BOOLE, KNASTER, TARSKI,
      FINSET_1, EQREL_1, MCART_1, NAT_1, ABIAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, MCART_1, DOMAIN_1, FINSET_1, SETFAM_1, CQC_SIM1, RELAT_1,
      FUNCT_1, FUNCT_2, FUNCOP_1, INT_1, NAT_1, EQREL_1, TRIANG_1, FUNCT_7,
      KNASTER;
 constructors DOMAIN_1, CQC_SIM1, REAL_1, TRIANG_1, AMI_1, KNASTER, INT_1,
      FUNCT_7, MEMBERED;
 clusters SUBSET_1, INT_1, FINSET_1, RELSET_1, PRALG_3, PUA2MSS1, TRIANG_1,
      MEMBERED, PARTFUN1, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve x, y, z, E, E1, E2, E3 for set,
        sE for Subset-Family of E,
        f for Function of E, E,
        k, l, m, n for Nat;

definition
 let i be number;
 attr i is even means
:: ABIAN:def 1
 ex j being Integer st i = 2*j;
 antonym i is odd;
end;

definition
 let n be Nat;
 redefine attr n is even means
:: ABIAN:def 2
   ex k st n = 2*k;
 antonym n is odd;
end;

definition
 cluster even Nat;
 cluster odd Nat;
 cluster even Integer;
 cluster odd Integer;
end;

theorem :: ABIAN:1
 for i being Integer
   holds i is odd iff ex j being Integer st i = 2*j+1;


definition
 let i be Integer;
 cluster 2*i -> even;
end;

definition
 let i be even Integer;
 cluster i+1 -> odd;
end;

definition
 let i be odd Integer;
 cluster i+1 -> even;
end;

definition
 let i be even Integer;
 cluster i-1 -> odd;
end;

definition
 let i be odd Integer;
 cluster i-1 -> even;
end;

definition
 let i be even Integer, j be Integer;
 cluster i*j -> even;
 cluster j*i -> even;
end;

definition
 let i, j be odd Integer;
 cluster i*j -> odd;
end;

definition
 let i, j be even Integer;
 cluster i+j -> even;
end;

definition
 let i be even Integer, j be odd Integer;
 cluster i+j -> odd;
 cluster j+i -> odd;
end;

definition
 let i, j be odd Integer;
 cluster i+j -> even;
end;

definition
 let i be even Integer, j be odd Integer;
 cluster i-j -> odd;
 cluster j-i -> odd;
end;

definition
 let i, j be odd Integer;
 cluster i-j -> even;
end;

definition
 let E, f, n;
 redefine func iter(f, n) -> Function of E, E;
end;

definition
  let A be set, B be with_non-empty_element set;
 cluster non-empty Function of A, B;
end;

definition
let A be non empty set, B be with_non-empty_element set,
    f be non-empty Function of A, B,
    a be Element of A;
 cluster f.a -> non empty;
end;

definition
 let X be non empty set;
 cluster bool X -> with_non-empty_element;
end;

theorem :: ABIAN:2
 for S being non empty Subset of NAT st 0 in S
  holds min S = 0;

theorem :: ABIAN:3
 for E being non empty set, f being Function of E, E,
     x being Element of E
  holds iter(f,0).x = x;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
 let f be Function;
 pred f has_a_fixpoint means
:: ABIAN:def 3
 ex x st x is_a_fixpoint_of f;
 antonym f has_no_fixpoint;
end;

definition
 let X be set, x be Element of X;
 attr x is covering means
:: ABIAN:def 4
 union x = union union X;
end;

theorem :: ABIAN:4
 sE is covering iff union sE = E;

definition
 let E;
 cluster non empty finite covering Subset-Family of E;
end;

theorem :: ABIAN:5
   for E being set, f being Function of E, E,
    sE being non empty covering Subset-Family of E
  st for X being Element of sE holds X misses f.:X
   holds f has_no_fixpoint;

definition
 let E, f;
 func =_f -> Equivalence_Relation of E means
:: ABIAN:def 5

  for x, y st x in E & y in E
   holds [x,y] in it iff ex k, l st iter(f,k).x = iter(f,l).y;
end;

theorem :: ABIAN:6
 for E being non empty set, f being Function of E, E,
     c being Element of Class =_f, e being Element of c holds f.e in c;

theorem :: ABIAN:7
 for E being non empty set, f being Function of E, E,
     c being Element of Class =_f, e being Element of c, n
   holds iter(f, n).e in c;

theorem :: ABIAN:8
   for E being non empty set, f being Function of E, E
  st f has_no_fixpoint
   ex E1, E2, E3 st E1 \/ E2 \/ E3 = E &
                    f.:E1 misses E1 & f.:E2 misses E2 & f.:E3 misses E3;