:: Fix-points in complete lattices
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 16, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: KNASTER:1
canceled;
theorem :: KNASTER:2
canceled;
theorem :: KNASTER:3
theorem Th4: :: KNASTER:4
theorem :: KNASTER:5
:: 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: :: KNASTER:6
theorem Th7: :: KNASTER:7
theorem Th8: :: KNASTER:8
theorem Th9: :: KNASTER:9
theorem Th10: :: KNASTER:10
theorem Th11: :: KNASTER:11
theorem Th12: :: KNASTER:12
theorem Th13: :: KNASTER:13
theorem :: KNASTER:14
definition
let L be
Lattice;
let f be
Function of the
carrier of
L,the
carrier of
L;
let x be
Element of
L;
let O be
Ordinal;
func f,
O +. x -> set means :
Def6:
:: 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 ) );
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:
:: 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 ) );
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 :: KNASTER:15
canceled;
theorem Th16: :: KNASTER:16
theorem Th17: :: KNASTER:17
theorem Th18: :: KNASTER:18
theorem Th19: :: KNASTER:19
theorem Th20: :: KNASTER:20
theorem Th21: :: KNASTER:21
theorem :: KNASTER:22
theorem :: KNASTER:23
:: deftheorem Def8 defines with_suprema KNASTER:def 8 :
:: deftheorem Def9 defines with_infima KNASTER:def 9 :
:: deftheorem Def10 defines latt KNASTER:def 10 :
theorem Th24: :: KNASTER:24
theorem Th25: :: KNASTER:25
theorem Th26: :: KNASTER:26
theorem Th27: :: KNASTER:27
theorem Th28: :: KNASTER:28
theorem Th29: :: KNASTER:29
theorem Th30: :: KNASTER:30
theorem Th31: :: KNASTER:31
theorem Th32: :: KNASTER:32
Lm1:
for O1, O2 being Ordinal holds
( O1 c< O2 or O1 = O2 or O2 c< O1 )
theorem Th33: :: KNASTER:33
theorem Th34: :: KNASTER:34
theorem Th35: :: KNASTER:35
theorem Th36: :: KNASTER:36
theorem Th37: :: KNASTER:37
theorem Th38: :: KNASTER:38
:: deftheorem Def11 defines FixPoints KNASTER:def 11 :
theorem Th39: :: KNASTER:39
theorem Th40: :: KNASTER:40
theorem Th41: :: KNASTER:41
theorem Th42: :: KNASTER:42
theorem :: KNASTER:43
:: deftheorem defines lfp KNASTER:def 12 :
:: deftheorem defines gfp KNASTER:def 13 :
theorem Th44: :: KNASTER:44
theorem Th45: :: KNASTER:45
theorem Th46: :: KNASTER:46
theorem :: KNASTER:47
theorem :: KNASTER:48
theorem Th49: :: KNASTER:49
theorem :: KNASTER:50
theorem :: KNASTER:51