:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
:: by Ewa Burakowska
::
:: Received July 8, 1993
:: Copyright (c) 1993 Association of Mizar Users
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 :: UNIALG_2:3
theorem :: UNIALG_2:4
theorem :: UNIALG_2:5
:: 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 :: UNIALG_2:6
canceled;
theorem Th7: :: UNIALG_2:7
theorem :: UNIALG_2:8
:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :
theorem Th9: :: UNIALG_2:9
theorem Th10: :: UNIALG_2:10
theorem :: UNIALG_2:11
theorem :: UNIALG_2:12
theorem Th13: :: UNIALG_2:13
theorem Th14: :: UNIALG_2:14
theorem Th15: :: UNIALG_2:15
theorem :: UNIALG_2:16
theorem Th17: :: UNIALG_2:17
:: 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: :: UNIALG_2:18
theorem :: UNIALG_2:19
theorem Th20: :: UNIALG_2:20
:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :
theorem :: 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 U0 be
Universal_Algebra;
func UniAlg_join U0 -> BinOp of
Sub U0 means :
Def16:
:: UNIALG_2:def 16
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:
:: UNIALG_2:def 17
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: :: UNIALG_2:27
theorem Th28: :: UNIALG_2:28
theorem Th29: :: UNIALG_2:29
theorem Th30: :: UNIALG_2:30
:: deftheorem defines UnSubAlLattice UNIALG_2:def 18 :