mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(topology/algebra/module/locally_convex): generalize `disjoint.exists_open_convexes` to locally convex spaces

Open ADedecker opened this issue 3 years ago • 1 comments

  • [x] depends on: #16747

Open in Gitpod

ADedecker avatar Oct 01 '22 21:10 ADedecker

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16747~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 11 '22 21:10 mathlib-dependent-issues-bot

Thanks!

bors merge

ocfnash avatar Oct 23 '22 12:10 ocfnash

Build failed (retrying...):

bors[bot] avatar Oct 23 '22 13:10 bors[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 23 '22 17:10 bors[bot]