Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-25 21:38 d4966769

View on Github →

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

Estimated changes

Modified src/geometry/manifold/charted_space.lean

added theorem charted_space.locally_compact

deleted def charted_space_core.local_homeomorph

added theorem mem_chart_target

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem model_with_corners.locally_compact

Modified src/order/filter/bases.lean

Modified src/topology/constructions.lean

added theorem filter.has_basis.prod_nhds'

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.symm_map_nhds_eq

Modified src/topology/metric_space/basic.lean

Modified src/topology/subset_properties.lean

added theorem compact_basis_nhds

added theorem locally_compact_space_of_has_basis

Modified src/topology/uniform_space/basic.lean