mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/convex/topology): minimize import

Open ADedecker opened this issue 3 years ago • 3 comments

Importing analysis/normed_space/finite_dimension was problematic for defining the strong operator topology because this needs quite a few facts about convexity but it has to be defined before continuous_linear_map.has_op_norm.

Open in Gitpod

ADedecker avatar Aug 14 '22 12:08 ADedecker

bors d+

sgouezel avatar Aug 14 '22 16:08 sgouezel

:v: ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Aug 14 '22 16:08 bors[bot]

bors merge

PatrickMassot avatar Aug 15 '22 08:08 PatrickMassot

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 15 '22 10:08 bors[bot]