unif cont -> cont

[affeldt-aist]

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

@zstone1 I wouldn't be surprised that this lemma is already somewhere...

[t6s]

I proved it before somewhere in my code, but not sure where it is..

[t6s]

Found in my older experiment on the equivalence between stdlib reals and mca reals; a bit shorter proof:

Section topology_ext.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Implicit Types U V : uniformType.

Lemma unif_continuous_continuous U V (f : U -> V) :
  unif_continuous f -> continuous f.
Proof.
rewrite /unif_continuous /cvg_to !nbhs_simpl => ucf.
rewrite /cvg_to /= => u X; rewrite !nbhs_simpl /= -!nbhs_entourageE.
case => Y /ucf /=; set Y' := (Y' in entourage Y') => eY' YX.
exists Y' => //.
rewrite /Y' /=.
rewrite -image_sub => v [] u' /= Yfuu' <-.
exact: YX.
Qed.
End topology_ext.