mathlib3
d4966769 - feat(geometry/manifold): manifold modelled on locally compact vector space is locally compact (#6394)

Commit

4 years ago

feat(geometry/manifold): manifold modelled on locally compact vector space is locally compact (#6394) Also connect `locally_compact_space` to `filter.has_basis`.

Author

urkud

Parents

8770f5c7

mathlib3 d4966769 - feat(geometry/manifold): manifold modelled on locally compact vector space is locally compact (#6394)

mathlib3
d4966769 - feat(geometry/manifold): manifold modelled on locally compact vector space is locally compact (#6394)