Commit 2024-01-09 09:25 4c48de09

View on Github →

chore(Topology/Maps): rename type variables (#9548) This file was mostly using Greek letters, but used letters X, Y, Z in comments and one theorem. Switch to using the latter consistently, per Zulip discussion.

Estimated changes

modified structure ClosedEmbedding
modified theorem Embedding.discreteTopology
modified theorem Embedding.map_nhds_eq
modified theorem Embedding.map_nhds_of_mem
modified theorem Embedding.mk'
modified theorem Embedding.tendsto_nhds_iff
modified structure Embedding
modified theorem Inducing.continuousAt_iff'
modified theorem Inducing.continuousAt_iff
modified theorem Inducing.dense_iff
modified theorem Inducing.isClosed_iff'
modified theorem Inducing.isClosed_iff
modified theorem Inducing.isClosed_preimage
modified theorem Inducing.isOpen_iff
modified theorem Inducing.mapClusterPt_iff
modified theorem Inducing.map_nhds_eq
modified theorem Inducing.map_nhds_of_mem
modified theorem Inducing.nhdsSet_eq_comap
modified theorem Inducing.nhds_eq_comap
modified theorem Inducing.tendsto_nhds_iff
modified structure Inducing
modified theorem IsClosedMap.of_inverse
modified def IsClosedMap
modified theorem IsOpenMap.image_mem_nhds
modified theorem IsOpenMap.mapsTo_interior
modified theorem IsOpenMap.nhds_le
modified theorem IsOpenMap.of_inverse
modified theorem IsOpenMap.of_nhds_le
modified theorem IsOpenMap.range_mem_nhds
modified def IsOpenMap
modified theorem OpenEmbedding.map_nhds_eq
modified theorem OpenEmbedding.of_comp
modified theorem OpenEmbedding.of_comp_iff
modified structure OpenEmbedding
modified theorem QuotientMap.of_inverse
modified def QuotientMap
modified theorem closedEmbedding_id
modified theorem embedding_id
modified theorem inducing_id
modified theorem inducing_iff_nhds
modified theorem inducing_induced
modified theorem isOpenMap_iff_nhds_le
modified theorem openEmbedding_id
modified theorem quotientMap_iff