bounded_on -> bounded_near #325
Description
In normedtype.v, bounded_on f F means f is bounded on at least one element on the filter F. Renaming it by bounded_near would be closer to its semantics, and allow the use of bounded_on f B for functions bounded on a bornology B (e.g.: simply bounded, uniformly bounded, ...) .
If legitimate, should this renaming be performed in PR 183 or in a new PR ?