let f be Function of REAL,REAL; :: thesis: for a, b being Real st b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) holds
f is continuous
let a, b be Real; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is continuous )
assume A2: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is continuous )
then A4: ( a - b < a & a < a + b ) by XREAL_1:44, XREAL_1:29;
assume A1: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is continuous
f = TriangularFS ((a - b),a,(a + b))
proof
A6: ( dom f = REAL & REAL = dom (TriangularFS ((a - b),a,(a + b))) ) by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = (TriangularFS ((a - b),a,(a + b))) . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = (TriangularFS ((a - b),a,(a + b))) . x )
assume x in dom f ; :: thesis: f . x = (TriangularFS ((a - b),a,(a + b))) . x
then x in REAL by FUNCT_2:def 1;
then reconsider x = x as Real ;
f . x = max (0,(1 - |.((x - a) / b).|)) by A1;
hence f . x = (TriangularFS ((a - b),a,(a + b))) . x by TR6, A2; :: thesis: verum
end;
hence f = TriangularFS ((a - b),a,(a + b)) by FUNCT_1:2, A6; :: thesis: verum
end;
hence f is continuous by A4, FUZNUM_1:30; :: thesis: verum