:: UNIALG_2 semantic presentation
theorem Th1: :: UNIALG_2:1
theorem Th2: :: UNIALG_2:2
:: deftheorem Def1 defines PFuncsDomHQN UNIALG_2:def 1 :
:: deftheorem Def2 defines are_similar UNIALG_2:def 2 :
theorem Th3: :: UNIALG_2:3
theorem Th4: :: UNIALG_2:4
theorem Th5: :: UNIALG_2:5
:: deftheorem Def3 defines Operations UNIALG_2:def 3 :
theorem Th6: :: UNIALG_2:6
:: 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 Th7: :: UNIALG_2:7
theorem Th8: :: UNIALG_2:8
:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :
theorem Th9: :: UNIALG_2:9
theorem Th10: :: UNIALG_2:10
theorem Th11: :: UNIALG_2:11
theorem Th12: :: UNIALG_2:12
theorem Th13: :: UNIALG_2:13
theorem Th14: :: UNIALG_2:14
theorem Th15: :: UNIALG_2:15
theorem Th16: :: UNIALG_2:16
theorem Th17: :: UNIALG_2:17
:: deftheorem Def9 defines UniAlgSetClosed UNIALG_2:def 9 :
:: deftheorem Def10 defines /\ UNIALG_2:def 10 :
:: deftheorem Def11 defines Constants UNIALG_2:def 11 :
:: deftheorem Def12 defines with_const_op UNIALG_2:def 12 :
theorem Th18: :: UNIALG_2:18
theorem Th19: :: UNIALG_2:19
theorem Th20: :: UNIALG_2:20
:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :
theorem Th21: :: UNIALG_2:21
theorem Th22: :: UNIALG_2:22
:: deftheorem Def14 defines "\/" UNIALG_2:def 14 :
theorem Th23: :: UNIALG_2:23
theorem Th24: :: UNIALG_2:24
theorem Th25: :: UNIALG_2:25
theorem Th26: :: UNIALG_2:26
:: deftheorem Def15 defines Sub UNIALG_2:def 15 :
definition
let c1 be
Universal_Algebra;
func UniAlg_join c1 -> BinOp of
Sub a1 means :
Def16:
:: UNIALG_2:def 16
for
b1,
b2 being
Element of
Sub a1 for
b3,
b4 being
strict SubAlgebra of
a1 st
b1 = b3 &
b2 = b4 holds
a2 . b1,
b2 = b3 "\/" b4;
existence
ex b1 being BinOp of Sub c1 st
for b2, b3 being Element of Sub c1
for b4, b5 being strict SubAlgebra of c1 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 "\/" b5
uniqueness
for b1, b2 being BinOp of Sub c1 st ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 "\/" b6 ) & ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 "\/" b6 ) holds
b1 = b2
end;
:: deftheorem Def16 defines UniAlg_join UNIALG_2:def 16 :
definition
let c1 be
Universal_Algebra;
func UniAlg_meet c1 -> BinOp of
Sub a1 means :
Def17:
:: UNIALG_2:def 17
for
b1,
b2 being
Element of
Sub a1 for
b3,
b4 being
strict SubAlgebra of
a1 st
b1 = b3 &
b2 = b4 holds
a2 . b1,
b2 = b3 /\ b4;
existence
ex b1 being BinOp of Sub c1 st
for b2, b3 being Element of Sub c1
for b4, b5 being strict SubAlgebra of c1 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 /\ b5
uniqueness
for b1, b2 being BinOp of Sub c1 st ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 /\ b6 ) & ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 /\ b6 ) holds
b1 = b2
end;
:: deftheorem Def17 defines UniAlg_meet UNIALG_2:def 17 :
theorem Th27: :: UNIALG_2:27
theorem Th28: :: UNIALG_2:28
theorem Th29: :: UNIALG_2:29
theorem Th30: :: UNIALG_2:30
:: deftheorem Def18 defines UnSubAlLattice UNIALG_2:def 18 :