Commit 2020-12-11 01:46 9e550f2d

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] -->