renaming `continuousFunType`?

[affeldt-aist]

analysis/theories/topology_theory/subspace_topology.v

Lines 688 to 691 in de99fb5

	#[short(type = "continuousFunType")]
	HB.structure Definition ContinuousFun {X Y : topologicalType}
	(A : set X) (B : set Y) :=
	{f of @isFun (subspace A) Y A B f & @Continuous (subspace A) Y f }.

Fun in the name is not really informative.
Moreover, we already have continuousType and it is easy to confuse both.

Wouldn't continuousSubspaceType of withinContinuousType be a better name?

@zstone1