Commit 2023-10-30 17:26 f6bb43b9

View on Github →

chore(Topology/Separation): rename type variables (#7589) This file was using a mix of Greek letters and standard math convention (X, Y, Z). connectedComponent_eq_iInter_clopen was even using X in comments and $\alpha$ in the code. As discussed on zulip, standardize on the latter.

Estimated changes

modified theorem CompactExhaustion.isClosed
modified theorem ConnectedSpace.infinite
modified theorem Continuous.closedEmbedding
modified theorem Continuous.ext_on
modified theorem Continuous.limUnder_eq
modified theorem ContinuousAt.eventually_ne
modified theorem Dense.diff_finite
modified theorem Dense.diff_finset
modified theorem Dense.diff_singleton
modified theorem Embedding.t2Space
modified theorem Embedding.t5Space
modified theorem Filter.Tendsto.limUnder_eq
modified theorem Filter.limUnder_eq_iff
modified theorem Inseparable.eq
modified theorem IsCompact.inter
modified theorem IsCompact.isClosed
modified theorem RegularSpace.ofBasis
modified theorem SeparatedNhds.comm
modified theorem SeparatedNhds.empty_left
modified theorem SeparatedNhds.empty_right
modified theorem SeparatedNhds.preimage
modified def SeparatedNhds
modified theorem Set.EqOn.of_subset_closure
modified theorem Set.Finite.t2_separation
modified theorem Set.Subsingleton.closure
modified theorem Specializes.eq
modified theorem T0Space.of_cover
modified theorem T0Space.of_open_cover
modified theorem biInter_basis_nhds
modified theorem closed_nhds_basis
modified theorem closure_singleton
modified theorem compl_singleton_mem_nhds
modified theorem continuousAt_update_of_ne
modified theorem continuousOn_update_iff
modified theorem discrete_of_t1_of_finite
modified theorem disjoint_lift'_closure_nhds
modified theorem disjoint_nested_nhds
modified theorem disjoint_nhdsSet_nhds
modified theorem disjoint_nhdsSet_nhdsSet
modified theorem disjoint_nhds_nhds
modified theorem disjoint_nhds_nhdsSet
modified theorem disjoint_nhds_pure
modified theorem disjoint_pure_nhds
modified theorem embedding_iff_inducing
modified theorem eqOn_closure₂'
modified theorem eqOn_closure₂
modified theorem eq_of_nhds_neBot
modified theorem eq_of_tendsto_nhds
modified theorem eventually_ne_nhds
modified theorem eventually_ne_nhdsWithin
modified theorem exists_compact_superset_iff
modified theorem exists_isOpen_xor'_mem
modified theorem hasBasis_nhds_closure
modified theorem hasBasis_opens_closure
modified theorem image_closure_of_isCompact
modified theorem infinite_of_mem_nhds
modified theorem injective_nhdsSet
modified theorem inseparable_eq_eq
modified theorem inseparable_iff_eq
modified theorem isClosedMap_const
modified theorem isClosed_diagonal
modified theorem isClosed_eq
modified theorem isClosed_setOf_inseparable
modified theorem isClosed_setOf_specializes
modified theorem isClosed_singleton
modified theorem isIrreducible_iff_singleton
modified theorem isOpen_compl_singleton
modified theorem isOpen_iff_ultrafilter'
modified theorem isOpen_ne
modified theorem isOpen_ne_fun
modified theorem isTopologicalBasis_clopen
modified theorem ker_nhds
modified theorem lift'_nhds_closure
modified theorem limUnder_nhdsWithin_id
modified theorem limUnder_nhds_id
modified theorem lim_eq
modified theorem lim_eq_iff
modified theorem lim_nhds
modified theorem lim_nhdsWithin
modified theorem locally_compact_of_compact
modified theorem nhdsSet_inj_iff
modified theorem nhdsSet_le_iff
modified theorem nhdsWithin_insert_of_ne
modified theorem nhdsWithin_of_mem_discrete
modified theorem nhds_basis_clopen
modified theorem nhds_eq_nhds_iff
modified theorem nhds_injective
modified theorem nhds_le_nhdsSet_iff
modified theorem nhds_le_nhds_iff
modified theorem normal_separation
modified theorem pairwise_disjoint_nhds
modified theorem pure_le_nhds_iff
modified theorem regularSpace_TFAE
modified theorem regularSpace_induced
modified theorem separatedNhds_iff_disjoint
modified theorem separated_by_continuous
modified theorem separated_by_openEmbedding
modified def specializationOrder
modified theorem specializes_comm
modified theorem specializes_eq_eq
modified theorem specializes_iff_eq
modified theorem specializes_iff_inseparable
modified theorem strictMono_nhdsSet
modified theorem subsingleton_closure
modified theorem t0Space_iff_inseparable
modified theorem t0Space_iff_nhds_injective
modified theorem t0Space_iff_not_inseparable
modified theorem t1Space_TFAE
modified theorem t1Space_antitone
modified theorem t2Space_iff_disjoint_nhds
modified theorem t2Space_iff_nhds
modified theorem t2_iff_isClosed_diagonal
modified theorem t2_iff_nhds
modified theorem t2_separation
modified theorem t2_separation_compact_nhds
modified theorem t2_separation_nhds
modified theorem tendsto_const_nhds_iff
modified theorem tendsto_nhds_unique'
modified theorem tendsto_nhds_unique