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

[affeldt-aist]

maybe continuousSubspaceType is better since the {within _, continuous} notation does not appear explicitly in the structure definition?

[affeldt-aist]

@mkerjean do you happen to have an opinion on the naming of this type? (you maybe foresee further extensions that could suggest a good name)

[mkerjean]

I don´t foresee any further extensions but I agree that continuousSubspaceType makes sense (and allows searching by name when working on a subspace).

[affeldt-aist]

It looks like this is not used in master (see the renaming PR #1902).
We do actually use it in the formalization of Cauchy-Lipschitz (fyi: @holgerthis, @yosakaon, @IshiguroYoshihiro ).