Commit 2023-10-12 10:52 1955a8e0

View on Github →

chore(Topology/LocallyCompact.lean): rename type variables (#7636) Greek letters for topological spaces are outdated, use letters X, Y, Z instead. Zulip discussion. Also generalise universes to Type* in two places.

Estimated changes

modified theorem compact_basis_nhds
modified theorem disjoint_nhds_cocompact
modified theorem exists_compact_between
modified theorem exists_compact_subset
modified theorem exists_compact_superset
modified theorem local_compact_nhds