:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received October 10, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem Th1: :: WAYBEL_2:1
theorem :: WAYBEL_2:2
theorem Th3: :: WAYBEL_2:3
theorem Th4: :: WAYBEL_2:4
theorem Th5: :: WAYBEL_2:5
theorem Th6: :: WAYBEL_2:6
theorem Th7: :: WAYBEL_2:7
theorem Th8: :: WAYBEL_2:8
theorem Th9: :: WAYBEL_2:9
theorem Th10: :: WAYBEL_2:10
theorem :: WAYBEL_2:11
theorem Th12: :: WAYBEL_2:12
theorem Th13: :: WAYBEL_2:13
theorem Th14: :: WAYBEL_2:14
theorem Th15: :: WAYBEL_2:15
theorem :: WAYBEL_2:16
theorem Th17: :: WAYBEL_2:17
theorem Th18: :: WAYBEL_2:18
theorem Th19: :: WAYBEL_2:19
theorem Th20: :: WAYBEL_2:20
:: deftheorem defines sup WAYBEL_2:def 1 :
definition
let L be non
empty RelStr ;
let J be
set ;
let f be
Function of
J,the
carrier of
L;
func FinSups f -> prenet of
L means :
Def2:
:: WAYBEL_2:def 2
ex
g being
Function of
Fin J,the
carrier of
L st
for
x being
Element of
Fin J holds
(
g . x = sup (f .: x) &
it = NetStr(#
(Fin J),
(RelIncl (Fin J)),
g #) );
existence
ex b1 being prenet of L ex g being Function of Fin J,the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
uniqueness
for b1, b2 being prenet of L st ex g being Function of Fin J,the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of Fin J,the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b1 = b2
end;
:: deftheorem Def2 defines FinSups WAYBEL_2:def 2 :
theorem :: WAYBEL_2:21
:: deftheorem Def3 defines "/\" WAYBEL_2:def 3 :
theorem Th22: :: WAYBEL_2:22
theorem Th23: :: WAYBEL_2:23
theorem Th24: :: WAYBEL_2:24
theorem Th25: :: WAYBEL_2:25
theorem Th26: :: WAYBEL_2:26
theorem Th27: :: WAYBEL_2:27
theorem Th28: :: WAYBEL_2:28
theorem :: WAYBEL_2:29
theorem :: WAYBEL_2:30
definition
let L be non
empty RelStr ;
func inf_op L -> Function of
[:L,L:],
L means :
Def4:
:: WAYBEL_2:def 4
for
x,
y being
Element of
L holds
it . x,
y = x "/\" y;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . x,y = x "/\" y
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . x,y = x "/\" y ) & ( for x, y being Element of L holds b2 . x,y = x "/\" y ) holds
b1 = b2
end;
:: deftheorem Def4 defines inf_op WAYBEL_2:def 4 :
theorem Th31: :: WAYBEL_2:31
theorem Th32: :: WAYBEL_2:32
theorem Th33: :: WAYBEL_2:33
definition
let L be non
empty RelStr ;
func sup_op L -> Function of
[:L,L:],
L means :
Def5:
:: WAYBEL_2:def 5
for
x,
y being
Element of
L holds
it . x,
y = x "\/" y;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . x,y = x "\/" y
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . x,y = x "\/" y ) & ( for x, y being Element of L holds b2 . x,y = x "\/" y ) holds
b1 = b2
end;
:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :
theorem Th34: :: WAYBEL_2:34
theorem Th35: :: WAYBEL_2:35
theorem :: WAYBEL_2:36
:: deftheorem Def6 defines satisfying_MC WAYBEL_2:def 6 :
:: deftheorem Def7 defines meet-continuous WAYBEL_2:def 7 :
theorem Th37: :: WAYBEL_2:37
theorem Th38: :: WAYBEL_2:38
theorem Th39: :: WAYBEL_2:39
theorem Th40: :: WAYBEL_2:40
theorem Th41: :: WAYBEL_2:41
theorem Th42: :: WAYBEL_2:42
theorem Th43: :: WAYBEL_2:43
theorem Th44: :: WAYBEL_2:44
theorem Th45: :: WAYBEL_2:45
theorem Th46: :: WAYBEL_2:46
theorem Th47: :: WAYBEL_2:47
theorem Th48: :: WAYBEL_2:48
theorem Th49: :: WAYBEL_2:49
theorem Th50: :: WAYBEL_2:50
theorem Th51: :: WAYBEL_2:51
theorem :: WAYBEL_2:52
theorem Th53: :: WAYBEL_2:53
theorem Th54: :: WAYBEL_2:54
theorem :: WAYBEL_2:55
Lm1:
for L being meet-continuous Semilattice
for x being Element of L holds x "/\" is directed-sups-preserving
theorem Th56: :: WAYBEL_2:56