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>

src/data/set/basic.lean

@@ -768,6 +768,9 @@ by finish [ext_iff]
 @[simp] lemma sep_univ {α} {p : α → Prop} : {a ∈ (univ : set α) | p a} = {a | p a} :=
 by { ext, simp }
 
+@[simp] lemma subset_singleton_iff {α : Type*} {s : set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
+iff.rfl
+
 /-! ### Lemmas about complement -/
 
 theorem mem_compl {s : set α} {x : α} (h : x ∉ s) : x ∈ sᶜ := h

src/topology/metric_space/basic.lean

@@ -668,6 +668,10 @@ theorem tendsto_at_top [nonempty β] [semilattice_sup β] {u : β → α} {a : 
 (at_top_basis.tendsto_iff nhds_basis_ball).trans $
   by { simp only [exists_prop, true_and], refl }
 
+lemma is_open_singleton_iff {X : Type*} [metric_space X] {x : X} :
+  is_open ({x} : set X) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x :=
+by simp [is_open_iff, subset_singleton_iff, mem_ball]
+
 end metric
 
 open metric

src/topology/order.lean

@@ -229,6 +229,14 @@ le_antisymm
 lemma eq_bot_of_singletons_open {t : topological_space α} (h : ∀ x, t.is_open {x}) : t = ⊥ :=
 bot_unique $ λ s hs, bUnion_of_singleton s ▸ is_open_bUnion (λ x _, h x)
 
+lemma forall_open_iff_discrete {X : Type*} [topological_space X] :
+  (∀ s : set X, is_open s) ↔ discrete_topology X :=
+⟨λ h, ⟨by { ext U , show is_open U ↔ true, simp [h U] }⟩, λ a, @is_open_discrete _ _ a⟩
+
+lemma singletons_open_iff_discrete {X : Type*} [topological_space X] :
+  (∀ a : X, is_open ({a} : set X)) ↔ discrete_topology X :=
+⟨λ h, ⟨eq_bot_of_singletons_open h⟩, λ a _, @is_open_discrete _ _ a _⟩
+
 end lattice
 
 section galois_connection

src/topology/separation.lean

@@ -93,6 +93,15 @@ begin
   apply is_closed_map.of_nonempty, intros s hs h2s, simp_rw [h2s.image_const, is_closed_singleton]
 end
 
+lemma discrete_of_t1_of_finite {X : Type*} [topological_space X] [t1_space X] [fintype X] :
+  discrete_topology X :=
+begin
+  apply singletons_open_iff_discrete.mp,
+  intros x,
+  rw [← is_closed_compl_iff, ← bUnion_of_singleton ({x} : set X)ᶜ],
+  exact is_closed_bUnion (finite.of_fintype _) (λ y _, is_closed_singleton)
+end
+
 /-- A T₂ space, also known as a Hausdorff space, is one in which for every
   `x ≠ y` there exists disjoint open sets around `x` and `y`. This is
   the most widely used of the separation axioms. -/