mathlib3

9e550f2d - feat(topology/separation): finite t1 spaces are discrete (#5298)

feat(topology/separation): finite t1 spaces are discrete (#5298) These lemmas should simplify the arguments of #4301 Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/discrete_topology/near/218932564 <!-- put comments you want to keep out of the PR commit here. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>