let f, g be Function of REAL,REAL; :: thesis: ( f is continuous & g is continuous implies min (f,g) is continuous )
assume A1: f is continuous ; :: thesis: ( not g is continuous or min (f,g) is continuous )
assume A2: g is continuous ; :: thesis: min (f,g) is continuous
for x being Real holds (min (f,g)) . x = min ((f . x),(g . x))
proof
let x be Real; :: thesis: (min (f,g)) . x = min ((f . x),(g . x))
reconsider x = x as Element of REAL by XREAL_0:def 1;
(min (f,g)) . x = min ((f . x),(g . x)) by COUSIN2:def 1;
hence (min (f,g)) . x = min ((f . x),(g . x)) ; :: thesis: verum
end;
hence min (f,g) is continuous by FUZZY_5:15, A1, A2; :: thesis: verum