Commit 2023-10-12 10:52 7b2163ce

View on Github →

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

Estimated changes

Modified Mathlib/Topology/GDelta.lean

modified theorem Finset.isGδ_compl

modified theorem IsClosed.isGδ

modified theorem IsClosed.isNowhereDense_iff

modified theorem IsGδ.inter

modified theorem IsGδ.union

modified def IsGδ

modified theorem IsMeagre.inter

modified theorem IsMeagre.mono

modified def IsMeagre

modified theorem IsNowhereDense.subset_of_closed_nowhereDense

modified def IsNowhereDense

modified theorem IsOpen.isGδ

modified theorem Set.Countable.isGδ_compl

modified theorem Set.Finite.isGδ

modified theorem Set.Finite.isGδ_compl

modified theorem Set.Subsingleton.isGδ_compl

modified theorem closed_isNowhereDense_iff_compl

modified theorem isGδ_biInter

modified theorem isGδ_biInter_of_open

modified theorem isGδ_biUnion

modified theorem isGδ_compl_singleton

modified theorem isGδ_empty

modified theorem isGδ_iInter

modified theorem isGδ_iInter_of_open

modified theorem isGδ_sInter

modified theorem isGδ_setOf_continuousAt

modified theorem isGδ_singleton

modified theorem isGδ_univ

modified theorem isNowhereDense_of_empty

modified theorem meagre_empty

modified theorem meagre_iUnion

modified theorem meagre_iff_countable_union_nowhereDense

modified theorem mem_residual_iff

modified def residual

modified theorem residual_of_dense_Gδ

modified theorem residual_of_dense_open