definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),(min (x,y)))
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),(min (x,y))) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = max ((1 - x),(min (x,y))) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = max (y,(min ((1 - x),(1 - y))))
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( y < 1 implies b1 . (x,y) = 0 ) & ( y = 1 implies b1 . (x,y) = 1 ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies b1 . (x,y) = 0 ) & ( y = 1 implies b1 . (x,y) = 1 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies b2 . (x,y) = 0 ) & ( y = 1 implies b2 . (x,y) = 1 ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x = 0 implies b1 . (x,y) = 1 ) & ( x > 0 implies b1 . (x,y) = 0 ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x = 0 implies b1 . (x,y) = 1 ) & ( x > 0 implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x = 0 implies b2 . (x,y) = 1 ) & ( x > 0 implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = 1
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = 1 ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = 1 ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = min (1,((1 - x) + y))
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = min (1,((1 - x) + y)) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = min (1,((1 - x) + y)) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = y ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = (1 - x) + (x * y)
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = (1 - x) + (x * y) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = (1 - x) + (x * y) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),y)
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),y) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = max ((1 - x),y) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y / x ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y / x ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = y / x ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = 0 ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b1 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b1 . (x,y) = y to_power x ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b1 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b1 . (x,y) = y to_power x ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b2 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b2 . (x,y) = y to_power x ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x < 1 implies b1 . (x,y) = 1 ) & ( x = 1 implies b1 . (x,y) = y ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x < 1 implies b1 . (x,y) = 1 ) & ( x = 1 implies b1 . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x < 1 implies b2 . (x,y) = 1 ) & ( x = 1 implies b2 . (x,y) = y ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = max ((1 - x),y) ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = max ((1 - x),y) ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = max ((1 - x),y) ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b1 . (x,y) = 0 ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b2 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b1 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b1 . (x,y) = 0 ) )
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b1 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b2 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
end;