Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-07 07:32 0eb49606

View on Github →

chore(topology/noetherian_space): golf (#18394) Also generalize noetherian_space.set to inducing.noetherian_space.

Estimated changes