naming of `closed_comp`

[affeldt-aist]

analysis/theories/topology_theory/topology_structure.v

Lines 787 to 788 in b1de71b

	Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) :
	{in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D).

shouldn't this lemma be called, for example, continuous_closed_preimage, because there is no explicit comp in the statement...

@zstone1

fyi: @holgerthies