`finSubCover` lacks documentation

[affeldt-aist]

https://github.com/math-comp/analysis/blob/22bb6cc4adc629f47b4ec03ef38eb2138ed2c9a5/theories/topology.v#L3013-L3016

[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.