feat(topology/discrete_quotient): add two lemmas (#8464)

Add lemmas `proj_bot_injective` and `proj_bot_bijective`, the former needed for the latter, and the latter needed in LTE.



Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>

Author: faenuccio

src/topology/discrete_quotient.lean

@@ -30,6 +30,8 @@ The type `discrete_quotient X` is endowed with an instance of a `semilattice_inf
 The partial ordering `A ≤ B` mathematically means that `B.proj` factors through `A.proj`.
 The top element `⊤` is the trivial quotient, meaning that every element of `X` is collapsed
 to a point. Given `h : A ≤ B`, the map `A → B` is `discrete_quotient.of_le h`.
+Whenever `X` is discrete, the type `discrete_quotient X` is also endowed with an instance of a
+`semilattice_inf_bot`, where the bot element `⊥` is `X` itself.
 
 Given `f : X → Y` and `h : continuous f`, we define a predicate `le_comap h A B` for
 `A : discrete_quotient X` and `B : discrete_quotient Y`, asserting that `f` descends to `A → B`.
@@ -198,6 +200,23 @@ lemma of_le_proj_apply {A B : discrete_quotient X} (h : A ≤ B) (x : X) :
 
 end of_le
 
+/--
+When X is discrete, there is a `semilattice_inf_bot` instance on `discrete_quotient X`
+-/
+instance [discrete_topology X] : semilattice_inf_bot (discrete_quotient X) :=
+{ bot :=
+  { rel := (=),
+    equiv := eq_equivalence,
+    clopen := λ x, is_clopen_discrete _ },
+  bot_le := by { rintro S a b (h : a = b), rw h, exact S.refl _ },
+  ..(infer_instance : semilattice_inf _) }
+
+lemma proj_bot_injective [discrete_topology X] :
+  function.injective (⊥ : discrete_quotient X).proj := λ a b h, quotient.exact' h
+
+lemma proj_bot_bijective [discrete_topology X] :
+  function.bijective (⊥ : discrete_quotient X).proj := ⟨proj_bot_injective, proj_surjective _⟩
+
 section map
 
 variables {Y : Type*} [topological_space Y] {f : Y → X}

src/topology/subset_properties.lean

@@ -1175,6 +1175,9 @@ begin
     exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩ }
 end
 
+@[simp] lemma is_clopen_discrete [discrete_topology α] (x : set α) : is_clopen x :=
+⟨is_open_discrete _, is_closed_discrete _⟩
+
 end clopen
 
 section preirreducible