Commit 2023-10-30 11:10 7d300cd8

View on Github →

chore(Topology/Compactness/SigmaCompact): rename type variables (#7730) Greek letters for topological spaces are outdated, use letters X, Y, Z instead. Zulip discussion.

Estimated changes

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

modified theorem CompactExhaustion.exists_mem

modified theorem CompactExhaustion.find_shiftr

modified theorem CompactExhaustion.mem_diff_shiftr_find

modified theorem CompactExhaustion.mem_find

modified theorem CompactExhaustion.mem_iff_find_le

modified def CompactExhaustion.shiftr

modified theorem Embedding.isSigmaCompact_iff

modified theorem Inducing.isSigmaCompact_iff

modified theorem IsClosed.sigmaCompactSpace

modified theorem IsCompact.isSigmaCompact

modified theorem IsSigmaCompact.image

modified theorem IsSigmaCompact.image_of_continuousOn

modified theorem IsSigmaCompact.of_isClosed_subset

modified def IsSigmaCompact

modified theorem SigmaCompactSpace.exists_compact_covering

modified theorem SigmaCompactSpace.of_countable

modified theorem Subtype.isSigmaCompact_iff

modified def compactCovering

modified theorem compactCovering_subset

modified theorem countable_cover_nhdsWithin_of_sigma_compact

modified theorem countable_cover_nhds_of_sigma_compact

modified theorem exists_mem_compactCovering

modified theorem iUnion_compactCovering

modified theorem isCompact_compactCovering

modified theorem isSigmaCompact_biUnion

modified theorem isSigmaCompact_empty

modified theorem isSigmaCompact_iUnion

modified theorem isSigmaCompact_iUnion_of_isCompact

modified theorem isSigmaCompact_iff_isSigmaCompact_univ

modified theorem isSigmaCompact_iff_sigmaCompactSpace

modified theorem isSigmaCompact_range

modified theorem isSigmaCompact_sUnion

modified theorem isSigmaCompact_sUnion_of_isCompact

modified theorem isSigmaCompact_univ

modified theorem isSigmaCompact_univ_iff