:: deftheorem Def5 defines dist_Func ASCOLI2:def 5 :
for S being non empty TopSpace
for T being non empty MetrSpace
for b₃ being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL holds
( b₃ = dist_Func (S,T) iff for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & b₃ . (f,g) = upper_bound (rng Dist) ) );