:: Subalgebras of a Order Sorted Algebra. {L}attice of Subalgebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: OSALG_2:1
theorem Th2: :: OSALG_2:2
:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def 1 :
:: deftheorem Def2 defines OSSubset OSALG_2:def 2 :
theorem Th3: :: OSALG_2:3
theorem Th4: :: OSALG_2:4
theorem Th5: :: OSALG_2:5
:: deftheorem defines OSConstants OSALG_2:def 3 :
theorem :: OSALG_2:6
canceled;
theorem :: OSALG_2:7
canceled;
theorem :: OSALG_2:8
canceled;
theorem :: OSALG_2:9
canceled;
theorem :: OSALG_2:10
canceled;
theorem Th11: :: OSALG_2:11
:: deftheorem Def4 defines OSCl OSALG_2:def 4 :
theorem Th12: :: OSALG_2:12
theorem Th13: :: OSALG_2:13
theorem :: OSALG_2:14
:: deftheorem Def5 defines OSConstants OSALG_2:def 5 :
theorem Th15: :: OSALG_2:15
theorem Th16: :: OSALG_2:16
theorem :: OSALG_2:17
theorem Th18: :: OSALG_2:18
theorem :: OSALG_2:19
theorem Th20: :: OSALG_2:20
:: deftheorem defines OSbool OSALG_2:def 6 :
:: deftheorem defines OSSubSort OSALG_2:def 7 :
theorem Th21: :: OSALG_2:21
theorem Th22: :: OSALG_2:22
:: deftheorem defines OSSubSort OSALG_2:def 8 :
theorem Th23: :: OSALG_2:23
:: deftheorem defines @ OSALG_2:def 9 :
theorem Th24: :: OSALG_2:24
theorem Th25: :: OSALG_2:25
:: deftheorem Def10 defines OSSubSort OSALG_2:def 10 :
theorem Th26: :: OSALG_2:26
theorem Th27: :: OSALG_2:27
theorem Th28: :: OSALG_2:28
:: deftheorem Def11 defines OSMSubSort OSALG_2:def 11 :
theorem Th29: :: OSALG_2:29
theorem :: OSALG_2:30
theorem Th31: :: OSALG_2:31
theorem Th32: :: OSALG_2:32
theorem Th33: :: OSALG_2:33
theorem Th34: :: OSALG_2:34
:: deftheorem OSALG_2:def 12 :
canceled;
:: deftheorem Def13 defines GenOSAlg OSALG_2:def 13 :
theorem Th35: :: OSALG_2:35
theorem Th36: :: OSALG_2:36
theorem Th37: :: OSALG_2:37
theorem :: OSALG_2:38
theorem Th39: :: OSALG_2:39
theorem Th40: :: OSALG_2:40
theorem Th41: :: OSALG_2:41
:: deftheorem Def14 defines "\/"_os OSALG_2:def 14 :
theorem Th42: :: OSALG_2:42
theorem Th43: :: OSALG_2:43
theorem Th44: :: OSALG_2:44
theorem Th45: :: OSALG_2:45
theorem Th46: :: OSALG_2:46
:: deftheorem Def15 defines OSSub OSALG_2:def 15 :
theorem Th47: :: OSALG_2:47
definition
let S1 be
OrderSortedSign;
let U0 be
non-empty OSAlgebra of
S1;
func OSAlg_join U0 -> BinOp of
(OSSub U0) means :
Def16:
:: OSALG_2:def 16
for
x,
y being
Element of
OSSub U0 for
U1,
U2 being
strict OSSubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 "\/"_os U2;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/"_os U2
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 "\/"_os U2 ) holds
b1 = b2
end;
:: deftheorem Def16 defines OSAlg_join OSALG_2:def 16 :
definition
let S1 be
OrderSortedSign;
let U0 be
non-empty OSAlgebra of
S1;
func OSAlg_meet U0 -> BinOp of
(OSSub U0) means :
Def17:
:: OSALG_2:def 17
for
x,
y being
Element of
OSSub U0 for
U1,
U2 being
strict OSSubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 /\ U2;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 /\ U2 ) holds
b1 = b2
end;
:: deftheorem Def17 defines OSAlg_meet OSALG_2:def 17 :
theorem Th48: :: OSALG_2:48
theorem Th49: :: OSALG_2:49
theorem Th50: :: OSALG_2:50
theorem Th51: :: OSALG_2:51
theorem Th52: :: OSALG_2:52
:: deftheorem defines OSSubAlLattice OSALG_2:def 18 :
theorem Th53: :: OSALG_2:53
theorem :: OSALG_2:54
theorem Th55: :: OSALG_2:55
theorem :: OSALG_2:56