:: Subalgebras of a Many Sorted Algebra. Lattice of Subalgebras
:: by Ewa Burakowska
::
:: Received April 25, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem :: MSUALG_2:1
canceled;
theorem Th2: :: MSUALG_2:2
:: deftheorem MSUALG_2:def 1 :
canceled;
:: deftheorem Def2 defines with_const_op MSUALG_2:def 2 :
:: deftheorem Def3 defines all-with_const_op MSUALG_2:def 3 :
:: deftheorem Def4 defines Constants MSUALG_2:def 4 :
:: deftheorem Def5 defines Constants MSUALG_2:def 5 :
:: deftheorem Def6 defines is_closed_on MSUALG_2:def 6 :
:: deftheorem Def7 defines opers_closed MSUALG_2:def 7 :
theorem Th3: :: MSUALG_2:3
:: deftheorem Def8 defines /. MSUALG_2:def 8 :
:: deftheorem Def9 defines Opers MSUALG_2:def 9 :
theorem Th4: :: MSUALG_2:4
theorem Th5: :: MSUALG_2:5
:: deftheorem Def10 defines MSSubAlgebra MSUALG_2:def 10 :
Lm1:
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S holds MSAlgebra(# the Sorts of U0,the Charact of U0 #) is MSSubAlgebra of U0
theorem :: MSUALG_2:6
theorem :: MSUALG_2:7
theorem Th8: :: MSUALG_2:8
theorem Th9: :: MSUALG_2:9
theorem Th10: :: MSUALG_2:10
theorem Th11: :: MSUALG_2:11
theorem :: MSUALG_2:12
theorem :: MSUALG_2:13
:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :
Lm2:
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A
:: deftheorem Def12 defines SubSort MSUALG_2:def 12 :
:: deftheorem defines @ MSUALG_2:def 13 :
theorem Th14: :: MSUALG_2:14
theorem Th15: :: MSUALG_2:15
:: deftheorem Def14 defines SubSort MSUALG_2:def 14 :
:: deftheorem Def15 defines MSSubSort MSUALG_2:def 15 :
theorem Th16: :: MSUALG_2:16
theorem Th17: :: MSUALG_2:17
theorem Th18: :: MSUALG_2:18
theorem Th19: :: MSUALG_2:19
theorem Th20: :: MSUALG_2:20
theorem Th21: :: MSUALG_2:21
:: deftheorem Def16 defines | MSUALG_2:def 16 :
:: deftheorem Def17 defines /\ MSUALG_2:def 17 :
:: deftheorem Def18 defines GenMSAlg MSUALG_2:def 18 :
theorem Th22: :: MSUALG_2:22
theorem Th23: :: MSUALG_2:23
theorem Th24: :: MSUALG_2:24
:: deftheorem Def19 defines "\/" MSUALG_2:def 19 :
theorem Th25: :: MSUALG_2:25
theorem Th26: :: MSUALG_2:26
theorem Th27: :: MSUALG_2:27
theorem Th28: :: MSUALG_2:28
theorem Th29: :: MSUALG_2:29
:: deftheorem Def20 defines MSSub MSUALG_2:def 20 :
definition
let S be non
empty non
void ManySortedSign ;
let U0 be
non-empty MSAlgebra of
S;
func MSAlg_join U0 -> BinOp of
MSSub U0 means :
Def21:
:: MSUALG_2:def 21
for
x,
y being
Element of
MSSub U0 for
U1,
U2 being
strict MSSubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 "\/" U2;
existence
ex b1 being BinOp of MSSub U0 st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/" U2
uniqueness
for b1, b2 being BinOp of MSSub U0 st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 "\/" U2 ) holds
b1 = b2
end;
:: deftheorem Def21 defines MSAlg_join MSUALG_2:def 21 :
definition
let S be non
empty non
void ManySortedSign ;
let U0 be
non-empty MSAlgebra of
S;
func MSAlg_meet U0 -> BinOp of
MSSub U0 means :
Def22:
:: MSUALG_2:def 22
for
x,
y being
Element of
MSSub U0 for
U1,
U2 being
strict MSSubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 /\ U2;
existence
ex b1 being BinOp of MSSub U0 st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2
uniqueness
for b1, b2 being BinOp of MSSub U0 st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 /\ U2 ) holds
b1 = b2
end;
:: deftheorem Def22 defines MSAlg_meet MSUALG_2:def 22 :
theorem Th30: :: MSUALG_2:30
theorem Th31: :: MSUALG_2:31
theorem Th32: :: MSUALG_2:32
theorem Th33: :: MSUALG_2:33
:: deftheorem defines MSSubAlLattice MSUALG_2:def 23 :
theorem Th34: :: MSUALG_2:34
theorem :: MSUALG_2:35
theorem Th36: :: MSUALG_2:36
theorem :: MSUALG_2:37
theorem :: MSUALG_2:38
theorem :: MSUALG_2:39
canceled;
theorem :: MSUALG_2:40
theorem :: MSUALG_2:41