Commit 2022-05-05 07:41 7eacca31
View on Github →feat(analysis/normed/normed_field): limit of ∥a * x∥ as ∥x∥ → ∞ (#13819)
These lemmas should use bornology.cobounded but we don't have an instance pseudo_metric_space α -> bornology α yet.
feat(analysis/normed/normed_field): limit of ∥a * x∥ as ∥x∥ → ∞ (#13819)
These lemmas should use bornology.cobounded but we don't have an instance pseudo_metric_space α -> bornology α yet.