Definition (Precompact)
This is a notion that in Metric Spaces can refer to Totally Bounded spaces or Relatively Compact spaces.
Remark
These two notions are only equivalent if we’re working with a Complete Metric Space (so in a Polish space, both are equivalent), otherwise they are different. It appears that: