For compact metric spaces, plenty of subtly different definitions converge to the same concept. Overtness can be viewed a a property dual to compactness. So is there a similar story for overt metric spaces?

Edit: Since Overtness is trivially true assuming the Law of the Excluded Middle, clearly the question is primarily interesting when we do not assume the LEM, which also means that the axiom of choice has to be weakened to countable or dependent choice. Any specific model where overtness is not trivially true is interesting, the setting does not have to be 100% constructive.