Commit 2022-04-01 22:20 6dad5f8c

feat(topology/bornology/basic): alternate way of defining a bornology by its bounded set (#13064) More precisely, this defines an alternative to https://leanprover-community.github.io/mathlib_docs/topology/bornology/basic.html#bornology.of_bounded (which is renamed bornology.of_bounded') which expresses the covering condition as containing the singletons, and factors the old version trough it to have a simpler proof. Note : I chose to add a prime to the old constructor because it's now defined in terms of the new one, so defeq works better this way (i.e lemma about the new constructor can be used whenever the old one is used).