Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_compact_of_compact_nhds

Modification history

2020-07-10 10:35
src/topology/separation.lean
chore(topology): rename compact to is_compact (#3356)
Modified locally_compact_of_compact_nhdsView on Github →
2019-11-12 11:23
src/topology/separation.lean
style(*): use notation `𝓝` for `nhds` (#1582) …
Modified locally_compact_of_compact_nhdsView on Github →
2019-10-12 20:07
src/topology/constructions.lean
refactor(topology): mild reorganization (#1541) …
Modified locally_compact_of_compact_nhdsView on Github →
2019-09-10 09:32
src/topology/constructions.lean
chore(topology): sanity_check pass (#1416) …
Modified locally_compact_of_compact_nhdsView on Github →
2018-10-01 14:40
analysis/topology/continuity.lean
refactor(analysis/topology): renamed compact_open to continuous_map; moved locally_compact to a more general position
Modified locally_compact_of_compact_nhdsView on Github →
2018-09-24 21:31
analysis/topology/compact_open.lean
feat(analysis/topology): locally compact spaces and the compact-open topology
Added locally_compact_of_compact_nhdsView on Github →