let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n)
for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let P be Subset of (TOP-REAL n); :: thesis: for Q being non empty Subset of (Euclid n)
for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let Q be non empty Subset of (Euclid n); :: thesis: for g being Function of I[01],((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let g be Function of I[01],((TOP-REAL n) | P); :: thesis: for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let f be Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q); :: thesis: ( P = Q & g is continuous & f = g implies f is uniformly_continuous )
assume that
A1: P = Q and
A2: ( g is continuous & f = g ) ; :: thesis: f is uniformly_continuous
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by A1, EUCLID:63;
hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; :: thesis: verum