:: Several Classes of {BCK}-algebras and Their Properties
:: by Tao Sun , Dahai Hu and Xiquan Liang
::
:: Received September 19, 2007
:: Copyright (c) 2007-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, BCIALG_1, BINOP_1, SUBSET_1, XXREAL_0, SUPINF_2,
XXREAL_2, CARD_FIL, BCIALG_3;
notations XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1;
constructors BCIALG_1;
registrations STRUCT_0, BCIALG_1;
requirements SUBSET;
begin :: The Basics of General Theory of commutative BCK-algebra
definition
let IT be non empty BCIStr_0;
attr IT is commutative means
:: BCIALG_3:def 1
for x,y being Element of IT holds x\(x\y ) = y\(y\x);
end;
registration
cluster BCI-EXAMPLE -> commutative;
end;
registration
cluster commutative for BCK-algebra;
end;
reserve X for BCK-algebra;
reserve x,y for Element of X;
reserve IT for non empty Subset of X;
theorem :: BCIALG_3:1
X is commutative BCK-algebra iff for x,y being Element of X holds
x\(x\y) <= y\(y\x);
theorem :: BCIALG_3:2
for X being BCK-algebra holds for x,y being Element of X holds x\
(x\y) <= y & x\(x\y) <= x;
theorem :: BCIALG_3:3
X is commutative BCK-algebra iff for x,y being Element of X holds
x\y = x\(y\(y\x));
theorem :: BCIALG_3:4
X is commutative BCK-algebra iff for x,y being Element of X holds
x\(x\y) = y\(y\(x\(x\y)));
theorem :: BCIALG_3:5
X is commutative BCK-algebra iff for x,y being Element of X st x
<= y holds x= y\(y\x);
theorem :: BCIALG_3:6
for X being non empty BCIStr_0 holds (X is commutative
BCK-algebra iff for x,y,z being Element of X holds x\(0.X\y) = x & (x\z)\(x\y)
= (y\z)\(y\x) );
theorem :: BCIALG_3:7
X is commutative BCK-algebra implies for x,y being Element of X st x\y
=x holds y\x=y;
theorem :: BCIALG_3:8
X is commutative BCK-algebra implies for x,y,a being Element of X
st y <= a holds (a\x)\(a\y) = y\x;
theorem :: BCIALG_3:9
X is commutative BCK-algebra implies for x,y being Element of X holds
(x\y=x iff y\(y\x)=0.X);
theorem :: BCIALG_3:10
X is commutative BCK-algebra implies for x,y being Element of X holds
x\(y\(y\x))=x\y & (x\y)\((x\y)\x)=x\y;
theorem :: BCIALG_3:11
X is commutative BCK-algebra implies for x,y,a being Element of X st x
<= a holds (a\y)\((a\y)\(a\x)) = (a\y)\(x\y);
definition
let X be BCI-algebra;
let a be Element of X;
attr a is being_greatest means
:: BCIALG_3:def 2
for x being Element of X holds x\a=0.X;
attr a is being_positive means
:: BCIALG_3:def 3
0.X\a=0.X;
end;
begin :: Several Classes of BCI-algebra---commutative BCI-algebra
definition
let IT be BCI-algebra;
attr IT is BCI-commutative means
:: BCIALG_3:def 4
for x,y being Element of IT st x\y= 0.IT holds x = y\(y\x);
attr IT is BCI-weakly-commutative means
:: BCIALG_3:def 5
for x,y being Element of IT holds (x\(x\y))\(0.IT\(x\y)) = y\(y\x);
end;
registration
cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative;
end;
registration
cluster BCI-commutative BCI-weakly-commutative for BCI-algebra;
end;
theorem :: BCIALG_3:12
for X being BCI-algebra holds ((ex a be Element of X st a is
being_greatest) implies X is BCK-algebra);
theorem :: BCIALG_3:13
for X being BCI-algebra holds (X is p-Semisimple implies X is
BCI-commutative & X is BCI-weakly-commutative );
theorem :: BCIALG_3:14
for X being commutative BCK-algebra holds X is BCI-commutative
BCI-algebra & X is BCI-weakly-commutative BCI-algebra;
theorem :: BCIALG_3:15
X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative;
theorem :: BCIALG_3:16
for X being BCI-algebra holds (X is BCI-commutative iff for x,y
being Element of X holds x\(x\y) = y\(y\(x\(x\y))) );
theorem :: BCIALG_3:17
for X being BCI-algebra holds (X is BCI-commutative iff for x,y
being Element of X holds (x\(x\y))\(y\(y\x)) = 0.X\(x\y) );
theorem :: BCIALG_3:18
for X being BCI-algebra holds (X is BCI-commutative iff for a being
Element of AtomSet(X),x,y being Element of BranchV(a) holds x\(x\y) = y\(y\x) )
;
theorem :: BCIALG_3:19
for X being non empty BCIStr_0 holds (X is BCI-commutative BCI-algebra
iff for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X = x & x\
(x\y) = y\(y\(x\(x\y))) );
theorem :: BCIALG_3:20
for X being BCI-algebra holds (X is BCI-commutative iff for x,y,z
being Element of X st x<=z & z\y<=z\x holds x<=y );
theorem :: BCIALG_3:21
for X being BCI-algebra holds (X is BCI-commutative iff for x,y,z
being Element of X st x<=y & x<=z holds x<=y\(y\z) );
begin :: Several Classes of BCK-algebra---bounded BCK-algebra
definition
let IT be BCK-algebra;
attr IT is bounded means
:: BCIALG_3:def 6
ex a be Element of IT st a is being_greatest;
end;
registration
cluster BCI-EXAMPLE -> bounded;
end;
registration
cluster bounded commutative for BCK-algebra;
end;
definition
let IT be bounded BCK-algebra;
attr IT is involutory means
:: BCIALG_3:def 7
for a being Element of IT st a is
being_greatest holds for x being Element of IT holds a\(a\x)=x;
end;
theorem :: BCIALG_3:22
for X being bounded BCK-algebra holds (X is involutory iff for a
being Element of X st a is being_greatest holds for x,y being Element of X
holds x\y = (a\y)\(a\x) );
theorem :: BCIALG_3:23
for X being bounded BCK-algebra holds (X is involutory iff for a
being Element of X st a is being_greatest holds for x,y being Element of X
holds x\(a\y) = y\(a\x) );
theorem :: BCIALG_3:24
for X being bounded BCK-algebra holds (X is involutory iff for a being
Element of X st a is being_greatest holds for x,y being Element of X holds x <=
a\y implies y <= a\x );
definition
let IT be BCK-algebra;
let a be Element of IT;
attr a is being_Iseki means
:: BCIALG_3:def 8
for x being Element of IT holds x\a=0.IT & a\x=a;
end;
definition
let IT be BCK-algebra;
attr IT is Iseki_extension means
:: BCIALG_3:def 9
ex a be Element of IT st a is being_Iseki;
end;
registration
cluster BCI-EXAMPLE -> Iseki_extension;
end;
:: Commutative Ideal
definition
let X be BCK-algebra;
mode Commutative-Ideal of X -> non empty Subset of X means
:: BCIALG_3:def 10
0.X in it
& for x,y,z being Element of X st (x\y)\z in it & z in it holds x\(y\(y\x)) in
it;
end;
theorem :: BCIALG_3:25
IT is Commutative-Ideal of X implies for x,y being Element of X st x\y
in IT holds x\(y\(y\x)) in IT;
theorem :: BCIALG_3:26
for X being BCK-algebra st IT is Commutative-Ideal of X holds IT
is Ideal of X;
theorem :: BCIALG_3:27
IT is Commutative-Ideal of X implies for x,y being Element of X st x\(
x\y) in IT holds (y\(y\x))\(x\y) in IT;
begin :: Several Classes of BCK-algebra---implicative BCK-algebra
definition
let IT be BCK-algebra;
attr IT is BCK-positive-implicative means
:: BCIALG_3:def 11
for x,y,z being Element of IT holds (x\y)\z=(x\z)\(y\z);
attr IT is BCK-implicative means
:: BCIALG_3:def 12
for x,y being Element of IT holds x \(y\x)=x;
end;
registration
cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative;
end;
registration
cluster Iseki_extension BCK-positive-implicative BCK-implicative bounded
commutative for BCK-algebra;
end;
theorem :: BCIALG_3:28
X is BCK-positive-implicative BCK-algebra iff for x,y being
Element of X holds x\y = (x\y)\y;
theorem :: BCIALG_3:29
X is BCK-positive-implicative BCK-algebra iff for x,y being
Element of X holds (x\(x\y))\(y\x) = x\(x\(y\(y\x)));
theorem :: BCIALG_3:30
X is BCK-positive-implicative BCK-algebra iff for x,y being Element of
X holds x\y = (x\y)\(x\(x\y));
theorem :: BCIALG_3:31
X is BCK-positive-implicative BCK-algebra iff for x,y,z being Element
of X holds (x\z)\(y\z) <= (x\y)\z;
theorem :: BCIALG_3:32
X is BCK-positive-implicative BCK-algebra iff for x,y being Element of
X holds x\y <= (x\y)\y;
theorem :: BCIALG_3:33
X is BCK-positive-implicative BCK-algebra iff for x,y being Element of
X holds (x\(x\(y\(y\x)))) <= (x\(x\y))\(y\x);
theorem :: BCIALG_3:34
X is BCK-implicative BCK-algebra iff X is commutative
BCK-algebra & X is BCK-positive-implicative BCK-algebra;
theorem :: BCIALG_3:35
X is BCK-implicative BCK-algebra iff for x,y being Element of X
holds (x\(x\y))\(x\y) = (y\(y\x));
theorem :: BCIALG_3:36
for X being non empty BCIStr_0 holds (X is BCK-implicative BCK-algebra
iff for x,y,z being Element of X holds x\(0.X\y) = x & (x\z)\(x\y) = ((y\z)\(y\
x))\(x\y) );
theorem :: BCIALG_3:37
for X being bounded BCK-algebra,a being Element of X st a is
being_greatest holds (X is BCK-implicative iff X is involutory & X is
BCK-positive-implicative );
theorem :: BCIALG_3:38
X is BCK-implicative BCK-algebra iff for x,y being Element of X holds
x\(x\(y\x)) = 0.X;
theorem :: BCIALG_3:39
X is BCK-implicative BCK-algebra iff for x,y being Element of X holds
(x\(x\y))\(x\y) = y\(y\(x\(x\y)));
theorem :: BCIALG_3:40
X is BCK-implicative BCK-algebra iff for x,y,z being Element of
X holds (x\z)\(x\y) = (y\z)\((y\x)\z);
theorem :: BCIALG_3:41
X is BCK-implicative BCK-algebra iff for x,y,z being Element of X
holds x\(x\(y\z)) = (y\z)\((y\z)\(x\z));
theorem :: BCIALG_3:42
X is BCK-implicative BCK-algebra iff for x,y being Element of X holds
(x\(x\y)) = (y\(y\x))\(x\y);
theorem :: BCIALG_3:43
for X being bounded commutative BCK-algebra,a being Element of X
st a is being_greatest holds (X is BCK-implicative iff for x being Element of X
holds (a\x)\((a\x)\x) = 0.X );
theorem :: BCIALG_3:44
for X being bounded commutative BCK-algebra,a being Element of X st a
is being_greatest holds (X is BCK-implicative iff for x being Element of X
holds x\(a\x) = x );
theorem :: BCIALG_3:45
for X being bounded commutative BCK-algebra,a being Element of X st a
is being_greatest holds (X is BCK-implicative iff for x being Element of X
holds (a\x)\x = (a\x) );
theorem :: BCIALG_3:46
for X being bounded commutative BCK-algebra,a being Element of X
st a is being_greatest holds (X is BCK-implicative iff for x,y being Element of
X holds (a\y)\((a\y)\x) = x\y );
theorem :: BCIALG_3:47
for X being bounded commutative BCK-algebra,a being Element of X
st a is being_greatest holds (X is BCK-implicative iff for x,y being Element of
X holds y\(y\x) = x\(a\y) );
theorem :: BCIALG_3:48
for X being bounded commutative BCK-algebra,a being Element of X st a
is being_greatest holds (X is BCK-implicative iff for x,y,z being Element of X
holds (x\(y\z))\(x\y) <= x\(a\z) );