chore(Topology): rename `IndiscreteTopology` to `HasIndiscreteTopology` by felixpernegger · Pull Request #40994 · leanprover-community/mathlib4

felixpernegger · 2026-06-24T10:36:59Z

Per naming convention. https://leanprover-community.github.io/contribute/naming.html#prop-valued-classes .

See this PR for further information.

Renaming discrete topology will be more involved, sinced its used much more widely

github-actions · 2026-06-24T10:38:17Z

PR summary 6be318ae38

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ HasIndiscreteTopology
+ HasIndiscreteTopology.isClosed_iff
+ HasIndiscreteTopology.isOpen_iff
+ HasIndiscreteTopology.nhds_eq
+ HasIndiscreteTopology.nnnorm_eq_zero'
+ HasIndiscreteTopology.norm_eq_zero'
+ HasIndiscreteTopology.of_forall_inseparable
+ HasIndiscreteTopology.of_forall_nnnorm_eq_zero
+ HasIndiscreteTopology.of_forall_nnnorm_eq_zero'
+ HasIndiscreteTopology.of_forall_norm_eq_zero
+ HasIndiscreteTopology.of_forall_norm_eq_zero'
+ HasIndiscreteTopology.toAlexandrovDiscrete
+ Pi.hasIndiscreteTopology
+ Prod.hasIndiscreteTopology
+ clusterPt_of_hasIndiscreteTopology
+ continuous_of_hasIndiscreteTopology
+ hasIndiscreteTopology_iff
+ hasIndiscreteTopology_iff_forall_nnnorm_eq_zero'
+ hasIndiscreteTopology_iff_forall_norm_eq_zero'
+ instance (priority := 100) HasIndiscreteTopology.pseudoMetrizableSpace [HasIndiscreteTopology X] :
+ instance (priority := 100) [HasIndiscreteTopology X] : PreirreducibleSpace X
+ instance (priority := 100) [HasIndiscreteTopology α] : NoetherianSpace α
+ instance (priority := 100) continuousDiv_of_hasIndiscreteTopology [TopologicalSpace H] [Div H]
+ instance (priority := 100) continuousInv_of_hasIndiscreteTopology [TopologicalSpace H] [Inv H]
+ instance (priority := 100) continuousMul_of_hasIndiscreteTopology [TopologicalSpace N] [Mul N]
+ instance (priority := 100) instCompactSpace [HasIndiscreteTopology X] : CompactSpace X
+ instance (priority := 100) topologicalGroup_of_hasIndiscreteTopology
+ instance : @HasIndiscreteTopology α ⊤ := @HasIndiscreteTopology.mk _ ⊤ rfl
+ instance : HasIndiscreteTopology (WithTopology α ⊤)
+ instance : HasIndiscreteTopology Empty := inferInstance
+ instance : HasIndiscreteTopology PEmpty := inferInstance
+ instance : HasIndiscreteTopology PUnit := inferInstance
+ instance [Nonempty Y] [HasIndiscreteTopology Y] : ContractibleSpace Y
+ instance [Nonempty α] [HasIndiscreteTopology α] : IsSimpleOrder (Opens α)
+ instance [TopologicalSpace α] [HasIndiscreteTopology α] : Subsingleton (SeparationQuotient α)
+ instance [TopologicalSpace α] [HasIndiscreteTopology α] {p : α → Prop} :
+ instance [TopologicalSpace α] [Subsingleton α] : HasIndiscreteTopology α
+ subsingleton_iff_hasIndiscreteTopology
++ hasIndiscreteTopology
++-- indiscreteTopology
- IndiscreteTopology.of_forall_nnnorm_eq_zero
- IndiscreteTopology.of_forall_nnnorm_eq_zero'
- IndiscreteTopology.of_forall_norm_eq_zero
- IndiscreteTopology.of_forall_norm_eq_zero'
- IndiscreteTopology.toAlexandrovDiscrete
- Pi.indiscreteTopology
- Prod.indiscreteTopology
- instance (priority := 100) IndiscreteTopology.pseudoMetrizableSpace [IndiscreteTopology X] :
- instance (priority := 100) [IndiscreteTopology X] : PreirreducibleSpace X
- instance (priority := 100) [IndiscreteTopology α] : NoetherianSpace α
- instance (priority := 100) continuousDiv_of_indiscreteTopology [TopologicalSpace H] [Div H]
- instance (priority := 100) continuousInv_of_indiscreteTopology [TopologicalSpace H] [Inv H]
- instance (priority := 100) continuousMul_of_indiscreteTopology [TopologicalSpace N] [Mul N]
- instance (priority := 100) instCompactSpace [IndiscreteTopology X] : CompactSpace X
- instance (priority := 100) topologicalGroup_of_indiscreteTopology
- instance : @IndiscreteTopology α ⊤ := @IndiscreteTopology.mk _ ⊤ rfl
- instance : IndiscreteTopology (WithTopology α ⊤)
- instance : IndiscreteTopology Empty := inferInstance
- instance : IndiscreteTopology PEmpty := inferInstance
- instance : IndiscreteTopology PUnit := inferInstance
- instance [Nonempty Y] [IndiscreteTopology Y] : ContractibleSpace Y
- instance [Nonempty α] [IndiscreteTopology α] : IsSimpleOrder (Opens α)
- instance [TopologicalSpace α] [IndiscreteTopology α] : Subsingleton (SeparationQuotient α)
- instance [TopologicalSpace α] [IndiscreteTopology α] {p : α → Prop} :
- instance [TopologicalSpace α] [Subsingleton α] : IndiscreteTopology α

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 6be318a).

+57 new declarations
−42 removed declarations

+ContractibleSpace.instOfNonemptyOfHasIndiscreteTopology
-ContractibleSpace.instOfNonemptyOfIndiscreteTopology
+EMetric.subsingleton_iff_hasIndiscreteTopology
+HasIndiscreteTopology
+HasIndiscreteTopology.casesOn
+HasIndiscreteTopology.eq_top
+HasIndiscreteTopology.eq_top_iff_indiscrete
+HasIndiscreteTopology.eq_top_uniformSpace
+HasIndiscreteTopology.isClosed_iff
+HasIndiscreteTopology.isOpen_iff
+HasIndiscreteTopology.mk
+HasIndiscreteTopology.nhds_eq
+HasIndiscreteTopology.nnnorm_eq_zero
+HasIndiscreteTopology.nnnorm_eq_zero'
+HasIndiscreteTopology.norm_eq_zero
+HasIndiscreteTopology.norm_eq_zero'
+HasIndiscreteTopology.of_forall_inseparable
+HasIndiscreteTopology.of_forall_nnnorm_eq_zero
+HasIndiscreteTopology.of_forall_nnnorm_eq_zero'
+HasIndiscreteTopology.of_forall_norm_eq_zero
+HasIndiscreteTopology.of_forall_norm_eq_zero'
+HasIndiscreteTopology.of_uniformity_eq_top
+HasIndiscreteTopology.rec
+HasIndiscreteTopology.recOn
+HasIndiscreteTopology.toAlexandrovDiscrete
+HasIndiscreteTopology.uniformContinuous
+Homeomorph.hasIndiscreteTopology
+Homeomorph.hasIndiscreteTopology_iff
-IndiscreteTopology.casesOn
-IndiscreteTopology.eq_top
-IndiscreteTopology.eq_top_iff_indiscrete
-IndiscreteTopology.eq_top_uniformSpace
-IndiscreteTopology.mk
-IndiscreteTopology.nnnorm_eq_zero
-IndiscreteTopology.norm_eq_zero
-IndiscreteTopology.of_forall_nnnorm_eq_zero
-IndiscreteTopology.of_forall_nnnorm_eq_zero'
-IndiscreteTopology.of_forall_norm_eq_zero
-IndiscreteTopology.of_forall_norm_eq_zero'
-IndiscreteTopology.of_uniformity_eq_top
-IndiscreteTopology.rec
-IndiscreteTopology.recOn
-IndiscreteTopology.toAlexandrovDiscrete
-IndiscreteTopology.uniformContinuous
+Pi.hasIndiscreteTopology
-Pi.indiscreteTopology
+Prod.hasIndiscreteTopology
-Prod.indiscreteTopology
+SeparationQuotient.instHasIndiscreteTopologySubtype
-SeparationQuotient.instIndiscreteTopologySubtype
+SeparationQuotient.instSubsingletonOfHasIndiscreteTopology
-SeparationQuotient.instSubsingletonOfIndiscreteTopology
+TopologicalSpace.HasIndiscreteTopology.pseudoMetrizableSpace
-TopologicalSpace.IndiscreteTopology.pseudoMetrizableSpace
+TopologicalSpace.Opens.instIsSimpleOrderOfNonemptyOfHasIndiscreteTopology
-TopologicalSpace.Opens.instIsSimpleOrderOfNonemptyOfIndiscreteTopology
+TopologicalSpace.instNoetherianSpaceOfHasIndiscreteTopology
-TopologicalSpace.instNoetherianSpaceOfIndiscreteTopology
+Topology.IsInducing.hasIndiscreteTopology
+clusterPt_of_hasIndiscreteTopology
+continuousAdd_of_hasIndiscreteTopology
-continuousAdd_of_indiscreteTopology
+continuousDiv_of_hasIndiscreteTopology
-continuousDiv_of_indiscreteTopology
+continuousInv_of_hasIndiscreteTopology
-continuousInv_of_indiscreteTopology
+continuousMul_of_hasIndiscreteTopology
-continuousMul_of_indiscreteTopology
+continuousNeg_of_hasIndiscreteTopology
-continuousNeg_of_indiscreteTopology
+continuousSub_of_hasIndiscreteTopology
-continuousSub_of_indiscreteTopology
+continuous_of_hasIndiscreteTopology
+hasIndiscreteTopology_iff
+hasIndiscreteTopology_iff_forall_nnnorm_eq_zero
+hasIndiscreteTopology_iff_forall_nnnorm_eq_zero'
+hasIndiscreteTopology_iff_forall_norm_eq_zero
+hasIndiscreteTopology_iff_forall_norm_eq_zero'
-indiscreteTopology_iff
-indiscreteTopology_iff_forall_nnnorm_eq_zero
-indiscreteTopology_iff_forall_norm_eq_zero
+instHasIndiscreteTopology
+instHasIndiscreteTopologyEmpty
+instHasIndiscreteTopologyOfSubsingleton
+instHasIndiscreteTopologyPEmpty
+instHasIndiscreteTopologyPUnit
+instHasIndiscreteTopologyWithTopologyTopTopologicalSpace
-instIndiscreteTopology
-instIndiscreteTopologyEmpty
-instIndiscreteTopologyOfSubsingleton
-instIndiscreteTopologyPEmpty
-instIndiscreteTopologyPUnit
-instIndiscreteTopologyWithTopologyTopTopologicalSpace
+instPreirreducibleSpaceOfHasIndiscreteTopology
-instPreirreducibleSpaceOfIndiscreteTopology
+topologicalAddGroup_of_hasIndiscreteTopology
-topologicalAddGroup_of_indiscreteTopology
+topologicalGroup_of_hasIndiscreteTopology
-topologicalGroup_of_indiscreteTopology

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 6be318ae38
Reference commit b587a4efdc

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

scholzhannah

Thank you for doing this! I have left some comments below.

scholzhannah · 2026-06-26T13:48:55Z

-alias ⟨_, IndiscreteTopology.of_forall_nnnorm_eq_zero'⟩ :=
-  indiscreteTopology_iff_forall_nnnorm_eq_zero'
-alias ⟨_, IndiscreteTopology.of_forall_nnnorm_eq_zero⟩ :=
-  indiscreteTopology_iff_forall_nnnorm_eq_zero
-attribute [to_additive existing IndiscreteTopology.of_forall_nnnorm_eq_zero]
-  IndiscreteTopology.of_forall_nnnorm_eq_zero'


I think we would also need deprecations for these old aliases, right?

scholzhannah · 2026-06-26T13:50:21Z

-alias ⟨_, IndiscreteTopology.of_forall_norm_eq_zero'⟩ :=
-  indiscreteTopology_iff_forall_norm_eq_zero'
-alias ⟨_, IndiscreteTopology.of_forall_norm_eq_zero⟩ :=
-  indiscreteTopology_iff_forall_norm_eq_zero
-attribute [to_additive existing IndiscreteTopology.of_forall_norm_eq_zero]
-  IndiscreteTopology.of_forall_norm_eq_zero'


Same as above probably?

scholzhannah · 2026-06-26T14:01:12Z

-@[to_additive indiscreteTopology_iff_forall_nnnorm_eq_zero]
-theorem indiscreteTopology_iff_forall_nnnorm_eq_zero' :
-    IndiscreteTopology E ↔ ∀ x : E, ‖x‖₊ = 0 := by
+@[to_additive hasIndiscreteTopology_iff_forall_nnnorm_eq_zero]
+theorem hasIndiscreteTopology_iff_forall_nnnorm_eq_zero' :
+    HasIndiscreteTopology E ↔ ∀ x : E, ‖x‖₊ = 0 := by
  simpa using nontrivialTopology_iff_exists_nnnorm_ne_zero' (E := E).not

+@[deprecated (since := "2026-06-24")]
+alias indiscreteTopology_iff_forall_nnnorm_eq_zero' :=
+  hasIndiscreteTopology_iff_forall_nnnorm_eq_zero'


It looks like you are always missing the deprecation for the declaration generated by to_additive. The style guide specifies how to properly do this.

Ok seems like add_depracations script is missing this

scholzhannah · 2026-06-26T14:15:20Z


-theorem indiscreteTopology_iff (h : X ≃ₜ Y) : IndiscreteTopology X ↔ IndiscreteTopology Y :=
-  ⟨fun _ ↦ h.indiscreteTopology, fun _ ↦ h.symm.indiscreteTopology⟩
+@[deprecated (since := "2026-06-24")] alias indiscreteTopology := Homeomorph.hasIndiscreteTopology


Suggested change

@[deprecated (since := "2026-06-24")] alias indiscreteTopology := Homeomorph.hasIndiscreteTopology

@[deprecated (since := "2026-06-24")] protected alias indiscreteTopology :=

Homeomorph.hasIndiscreteTopology

Here and below.

mathlib-merge-conflicts · 2026-07-08T22:44:10Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-07-14T22:49:53Z

This pull request has conflicts, please merge master and resolve them.

j-loreaux · 2026-07-15T02:51:34Z

This needs a Zulip discussion, as almost the entirety of the topology library does not use this convention for Prop-valued mixins.

felixpernegger added 2 commits June 24, 2026 11:39

.

5c7ac9b

.

fad6e55

github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jun 24, 2026

felixpernegger added 2 commits June 24, 2026 13:38

.

8f05925

.

23d9255

scholzhannah reviewed Jun 26, 2026

View reviewed changes

scholzhannah added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 26, 2026

scholzhannah self-assigned this Jun 26, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 8, 2026

Merge branch 'master' into renameindiscrete

6be318a

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 14, 2026

grunweg added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Jul 15, 2026

Navigation Menu

Uh oh!

chore(Topology): rename `IndiscreteTopology` to `HasIndiscreteTopology` - #40994

chore(Topology): rename `IndiscreteTopology` to `HasIndiscreteTopology`#40994
felixpernegger wants to merge 5 commits into
leanprover-community:masterfrom
felixpernegger:renameindiscrete

felixpernegger commented Jun 24, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 24, 2026 •

edited

Loading

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

scholzhannah left a comment

Uh oh!

scholzhannah Jun 26, 2026

Uh oh!

scholzhannah Jun 26, 2026

Uh oh!

scholzhannah Jun 26, 2026

Uh oh!

felixpernegger Jun 26, 2026

Uh oh!

scholzhannah Jun 26, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jul 8, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jul 14, 2026

Uh oh!

j-loreaux commented Jul 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

	@[deprecated (since := "2026-06-24")] alias indiscreteTopology := Homeomorph.hasIndiscreteTopology
	@[deprecated (since := "2026-06-24")] protected alias indiscreteTopology :=
	Homeomorph.hasIndiscreteTopology

Uh oh!

Conversation

felixpernegger commented Jun 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 6be318ae38

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

scholzhannah left a comment

Choose a reason for hiding this comment

Uh oh!

scholzhannah Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

scholzhannah Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

scholzhannah Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

felixpernegger Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

scholzhannah Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-merge-conflicts Bot commented Jul 8, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jul 14, 2026

Uh oh!

j-loreaux commented Jul 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

felixpernegger commented Jun 24, 2026 •

edited

Loading

github-actions Bot commented Jun 24, 2026 •

edited

Loading