begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines PFuncsDomHQN UNIALG_2:def 1 :
:: deftheorem Def2 defines are_similar UNIALG_2:def 2 :
theorem
theorem
theorem
:: deftheorem defines Operations UNIALG_2:def 3 :
:: deftheorem Def4 defines is_closed_on UNIALG_2:def 4 :
:: deftheorem Def5 defines opers_closed UNIALG_2:def 5 :
:: deftheorem Def6 defines /. UNIALG_2:def 6 :
:: deftheorem Def7 defines Opers UNIALG_2:def 7 :
theorem
canceled;
theorem Th7:
theorem
:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :
theorem Th9:
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
:: deftheorem Def9 defines UniAlgSetClosed UNIALG_2:def 9 :
:: deftheorem Def10 defines /\ UNIALG_2:def 10 :
:: deftheorem defines Constants UNIALG_2:def 11 :
:: deftheorem Def12 defines with_const_op UNIALG_2:def 12 :
theorem Th18:
theorem
theorem Th20:
:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :
theorem
theorem Th22:
:: deftheorem Def14 defines "\/" UNIALG_2:def 14 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
:: deftheorem Def15 defines Sub UNIALG_2:def 15 :
definition
let U0 be
Universal_Algebra;
func UniAlg_join U0 -> BinOp of
(Sub U0) means :
Def16:
for
x,
y being
Element of
Sub U0 for
U1,
U2 being
strict SubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 "\/" U2;
existence
ex b1 being BinOp of (Sub U0) st
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/" U2
uniqueness
for b1, b2 being BinOp of (Sub U0) st ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/" U2 ) & ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 "\/" U2 ) holds
b1 = b2
end;
:: deftheorem Def16 defines UniAlg_join UNIALG_2:def 16 :
definition
let U0 be
Universal_Algebra;
func UniAlg_meet U0 -> BinOp of
(Sub U0) means :
Def17:
for
x,
y being
Element of
Sub U0 for
U1,
U2 being
strict SubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 /\ U2;
existence
ex b1 being BinOp of (Sub U0) st
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2
uniqueness
for b1, b2 being BinOp of (Sub U0) st ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2 ) & ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 /\ U2 ) holds
b1 = b2
end;
:: deftheorem Def17 defines UniAlg_meet UNIALG_2:def 17 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem defines UnSubAlLattice UNIALG_2:def 18 :