feat: two topological lemmas for finite (co)dimension subspaces (leanprover-community#38461)

My application for these (Fredholm operators) is a bit far away, but I'm sure they will be useful in other contexts. Technically one of them could be deduced from the other, but the reduction is longer than the direct two-line proof.

Author: ADedecker

Mathlib/Topology/Algebra/Module/FiniteDimension.lean

@@ -536,6 +536,21 @@ theorem Submodule.closed_of_finiteDimensional
   haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
   s.complete_of_finiteDimensional.isClosed
 
+/-- If `s` is a closed subspace with finite codimension, any subspace containing `s` is closed. -/
+theorem Submodule.isClosed_mono_of_finiteDimensional_quotient
+    {s t : Submodule 𝕜 E} [FiniteDimensional 𝕜 (E ⧸ s)] (s_closed : IsClosed (s : Set E))
+    (s_le_t : s ≤ t) :
+    IsClosed (t : Set E) := by
+  rw [show t = comap s.mkQ (map s.mkQ t) by simpa]
+  exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk
+
+/-- The supremum of a closed subspace and a finite dimensional subspace is closed. -/
+theorem Submodule.isClosed_sup_finiteDimensional
+    (s t : Submodule 𝕜 E) (hs : IsClosed (s : Set E)) [ht : FiniteDimensional 𝕜 t] :
+    IsClosed ((s ⊔ t : Submodule 𝕜 E) : Set E) := by
+  rw [← comap_map_mkQ]
+  exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk
+
 /-- An injective linear map with finite-dimensional domain is a closed embedding. -/
 theorem LinearMap.isClosedEmbedding_of_injective [T2Space E] [FiniteDimensional 𝕜 E] {f : E →ₗ[𝕜] F}
     (hf : LinearMap.ker f = ⊥) : IsClosedEmbedding f :=