Commit 2023-11-30 20:57 85239de6

View on Github →

chore(Topology/{Compactness/Compact}, Irreducible}): rename type variables (#7591) X, Y, Z are standard mathematical names for topological spaces. As discussed on zulip, let us rename them. As a drive-by commit, re-use the declared variables $\iota$, $s$ and $t$ (more) when stating theorems.

Estimated changes

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Compactness/Compact.lean

modified theorem Bornology.inCompact.isBounded_iff

modified def Bornology.inCompact

modified theorem ClosedEmbedding.isCompact_preimage

modified theorem ClosedEmbedding.tendsto_cocompact

modified theorem CompactSpace.elim_nhds_subcover

modified theorem Embedding.isCompact_iff

modified theorem Filter.Tendsto.isCompact_insert_range

modified theorem Filter.Tendsto.isCompact_insert_range_of_cocompact

modified theorem Filter.Tendsto.isCompact_insert_range_of_cofinite

modified def Filter.coclosedCompact

modified def Filter.cocompact

modified theorem Filter.cocompact_eq_bot

modified theorem Filter.cocompact_eq_cofinite

modified theorem Filter.cocompact_le_coclosedCompact

modified theorem Filter.cocompact_le_cofinite

modified theorem Filter.cocompact_neBot_iff

modified theorem Filter.comap_cocompact_le

modified theorem Filter.coprodᵢ_cocompact

modified theorem Filter.hasBasis_cocompact

modified theorem Filter.mem_coclosedCompact

modified theorem Filter.mem_coclosed_compact'

modified theorem Filter.mem_cocompact'

modified theorem Filter.mem_cocompact

modified theorem Finset.isCompact_biUnion

modified theorem Inducing.isCompact_iff

modified theorem Inducing.isCompact_preimage

modified theorem IsClosed.exists_minimal_nonempty_closed_subset

modified theorem IsClosed.isCompact

modified theorem IsCompact.adherence_nhdset

modified theorem IsCompact.compl_mem_cocompact

modified theorem IsCompact.compl_mem_sets

modified theorem IsCompact.compl_mem_sets_of_nhdsWithin

modified theorem IsCompact.disjoint_nhdsSet_left

modified theorem IsCompact.disjoint_nhdsSet_right

modified theorem IsCompact.elim_finite_subcover

modified theorem IsCompact.elim_finite_subcover_image

modified theorem IsCompact.elim_finite_subfamily_closed

modified theorem IsCompact.elim_nhds_subcover'

modified theorem IsCompact.elim_nhds_subcover

modified theorem IsCompact.eventually_forall_of_forall_eventually

modified theorem IsCompact.finite

modified theorem IsCompact.finite_of_discrete

modified theorem IsCompact.image

modified theorem IsCompact.image_of_continuousOn

modified theorem IsCompact.induction_on

modified theorem IsCompact.inter_iInter_nonempty

modified theorem IsCompact.le_nhds_of_unique_clusterPt

modified theorem IsCompact.mem_nhdsSet_prod_of_forall

modified theorem IsCompact.mem_prod_nhdsSet_of_forall

modified theorem IsCompact.ne_univ

modified theorem IsCompact.nhdsSet_prod_eq

modified theorem IsCompact.nhdsSet_prod_eq_biSup

modified theorem IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed

modified theorem IsCompact.prod

modified theorem IsCompact.prod_nhdsSet_eq_biSup

modified theorem IsCompact.tendsto_nhds_of_unique_mapClusterPt

modified def IsCompact

modified theorem LocallyFinite.finite_nonempty_inter_compact

modified theorem LocallyFinite.finite_nonempty_of_compact

modified theorem LocallyFinite.finite_of_compact

modified theorem Set.Finite.isCompact_biUnion

modified theorem Set.Finite.isCompact_sUnion

modified theorem Set.Subsingleton.isCompact

modified theorem Subtype.isCompact_iff

modified theorem cluster_point_of_compact

modified theorem exists_nhds_ne_inf_principal_neBot

modified theorem exists_nhds_ne_neBot

modified theorem exists_subset_nhds_of_compactSpace

modified theorem exists_subset_nhds_of_isCompact'

modified theorem finite_cover_nhds

modified theorem finite_cover_nhds_interior

modified theorem finite_of_compact_of_discrete

modified theorem generalized_tube_lemma

modified theorem isClosedMap_fst_of_compactSpace

modified theorem isClosedMap_snd_of_compactSpace

modified theorem isCompact_accumulate

modified theorem isCompact_diagonal

modified theorem isCompact_empty

modified theorem isCompact_iUnion

modified theorem isCompact_iff_compactSpace

modified theorem isCompact_iff_finite

modified theorem isCompact_iff_isCompact_univ

modified theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis

modified theorem isCompact_pi_infinite

modified theorem isCompact_range

modified theorem isCompact_singleton

modified theorem isCompact_univ

modified theorem isCompact_univ_iff

modified theorem isCompact_univ_pi

modified theorem le_nhds_of_unique_clusterPt

modified theorem nhdsSet_prod_le

modified theorem noncompactSpace_of_neBot

modified theorem noncompact_univ

modified theorem not_compactSpace_iff

modified theorem tendsto_nhds_of_unique_mapClusterPt

Modified Mathlib/Topology/Irreducible.lean

modified theorem IrreducibleSpace.isIrreducible_univ

modified theorem IsIrreducible.image

modified theorem IsIrreducible.isPreirreducible

modified theorem IsIrreducible.nonempty

modified def IsIrreducible

modified theorem IsPreirreducible.image

modified theorem IsPreirreducible.interior

modified theorem IsPreirreducible.open_subset

modified theorem IsPreirreducible.preimage

modified theorem IsPreirreducible.subset_irreducible

modified def IsPreirreducible

modified theorem Set.Subsingleton.isPreirreducible

modified theorem Subtype.irreducibleSpace

modified theorem Subtype.preirreducibleSpace

modified theorem eq_irreducibleComponent

modified theorem exists_preirreducible

modified def irreducibleComponent

modified theorem irreducibleComponent_mem_irreducibleComponents

modified theorem irreducibleComponent_property

modified def irreducibleComponents

modified theorem irreducibleComponents_eq_maximals_closed

modified theorem irreducibleSpace_def

modified theorem isClosed_irreducibleComponent

modified theorem isClosed_of_mem_irreducibleComponents

modified theorem isIrreducible_iff_closure

modified theorem isIrreducible_iff_sInter

modified theorem isIrreducible_iff_sUnion_closed

modified theorem isIrreducible_irreducibleComponent

modified theorem isIrreducible_singleton

modified theorem isPreirreducible_empty

modified theorem isPreirreducible_iff_closed_union_closed

modified theorem isPreirreducible_iff_closure

modified theorem isPreirreducible_singleton

modified theorem mem_irreducibleComponent

modified theorem nonempty_preirreducible_inter

modified theorem subset_closure_inter_of_isPreirreducible_of_isOpen

Modified Mathlib/Topology/Separation.lean