Commit 2023-10-30 11:10 553dd6bd

View on Github →

chore(Topology/Clopen): rename type variables (#7921) This file was using a mixture of Greek letters and letters X, Y, Z. Switch to using the latter consistently, per Zulip discussion. Best reviewed commit by commit; each is self-contained and should be quick to review.

Estimated changes

Modified Mathlib/Topology/Clopen.lean

modified theorem ContinuousOn.preimage_clopen_of_clopen

modified theorem IsClopen.compl

modified theorem IsClopen.diff

modified theorem IsClopen.inter

modified theorem IsClopen.preimage

modified theorem IsClopen.prod

modified theorem IsClopen.union

modified def IsClopen

modified theorem Set.Finite.isClopen_biInter

modified theorem Set.Finite.isClopen_biUnion

modified theorem isClopen_biInter_finset

modified theorem isClopen_biUnion_finset

modified theorem isClopen_compl_iff

modified theorem isClopen_discrete

modified theorem isClopen_empty

modified theorem isClopen_iInter_of_finite

modified theorem isClopen_iUnion_of_finite

modified theorem isClopen_iff_frontier_eq_empty

modified theorem isClopen_inter_of_disjoint_cover_clopen

modified theorem isClopen_range_inl

modified theorem isClopen_range_inr

modified theorem isClopen_range_sigmaMk

modified theorem isClopen_univ