Induced discrete topology

Stream: Is there code for X?

[Ashvni Narayanan]

Hello, I am looking for an updated version of discrete_topology_induced, which was removed in the PR : https://github.com/leanprover-community/mathlib/pull/18312

Any help is appreciated, thank you!

[Yaël Dillies]

Have you looked at the changelog?

[Yaël Dillies]

Indeed, there's no more information there... @Yury G. Kudryashov, what is the substitute supposed to be?

[Yaël Dillies]

(also, writing #18312 instead https://github.com/leanprover-community/mathlib/pull/18312 makes it more obvious that you're referencing a PR)

[Ashvni Narayanan]

I think I found a way using embedding.discrete_topology