begin
theorem
canceled;
theorem
canceled;
theorem
begin
theorem Th4:
theorem
:: deftheorem KNASTER:def 1 :
canceled;
:: deftheorem KNASTER:def 2 :
canceled;
:: deftheorem Def3 defines c=-monotone KNASTER:def 3 :
:: deftheorem defines lfp KNASTER:def 4 :
:: deftheorem defines gfp KNASTER:def 5 :
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
scheme
Knaster{
F1()
-> set ,
F2(
set )
-> set } :
ex
D being
set st
(
F2(
D)
= D &
D c= F1() )
provided
A1:
for
X,
Y being
set st
X c= Y holds
F2(
X)
c= F2(
Y)
and A2:
F2(
F1())
c= F1()
theorem Th11:
theorem Th12:
theorem Th13:
theorem
begin
definition
let L be
Lattice;
let f be
Function of the
carrier of
L,the
carrier of
L;
let x be
Element of ;
let O be
Ordinal;
func f,
O +. x -> set means :
Def6:
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 ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = 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 ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = 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 ) ) & ex L0 being T-Sequence st
( b2 = 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 ) ) holds
b1 = b2;
func f,
O -. x -> set means :
Def7:
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 ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = 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 ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = 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 ) ) & ex L0 being T-Sequence st
( b2 = 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 ) ) holds
b1 = b2;
end;
:: deftheorem Def6 defines +. KNASTER:def 6 :
:: deftheorem Def7 defines -. KNASTER:def 7 :
theorem
canceled;
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
:: deftheorem Def8 defines with_suprema KNASTER:def 8 :
:: deftheorem Def9 defines with_infima KNASTER:def 9 :
:: deftheorem Def10 defines latt KNASTER:def 10 :
begin
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
Lm1:
for O1, O2 being Ordinal holds
( O1 c< O2 or O1 = O2 or O2 c< O1 )
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def11 defines FixPoints KNASTER:def 11 :
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
:: deftheorem defines lfp KNASTER:def 12 :
:: deftheorem defines gfp KNASTER:def 13 :
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
begin
theorem Th49:
theorem
theorem