finSubCover lacks documentation

[affeldt-aist]

analysis/theories/topology.v

Lines 3013 to 3016 in 22bb6cc

	Definition finSubCover (I : choiceType) (D : set I)
	U (F : I -> set U) (A : set U) :=
	exists2 D' : {fset I}, {subset D' <= D} &
	A `<=` \bigcup_(i in [set i | i \in D']) F i.

[t6s]

I suspect the reason this definition is not documented might be that it is not a good definition.
The name suggests that it is pinpointing a (finite) subcover of some cover, but there is no such original cover in the definition.

Definition hasFinSubCover (I : choiceType) (D : set I)
    U (F : I -> set U) :=
  exists2 D' : {fset I}, {subset D' <= D} &
    \bigcup_(i in D) F i =
    \bigcup_(i in [set i | i \in D']) F i.

Something like this would be more clear-cut. I suggest also adding the prefix has, if it is not violating the naming convention in mathcomp-analysis.