feat(Topology/Algebra/Module): add Submodule.ClosedComplemented.of_finiteDimensional_of_le (leanprover-community#39380)

Submodules of finite-dimensional closed, complemented submodules are closed and complemented.

Author: JonBannon

Mathlib/Topology/Algebra/Module/FiniteDimension.lean

@@ -740,6 +740,14 @@ theorem Submodule.ClosedComplemented.of_finiteDimensional_quotient {p : Submodul
 alias Submodule.ClosedComplemented.of_quotient_finiteDimensional :=
   Submodule.ClosedComplemented.of_finiteDimensional_quotient
 
+lemma Submodule.ClosedComplemented.of_finiteDimensional_of_le
+    {A B : Submodule 𝕜 E} [FiniteDimensional 𝕜 A] (hA : A.ClosedComplemented) [T2Space A]
+    (hB : B ≤ A) : B.ClosedComplemented := by
+  obtain ⟨p, hp⟩ := hA
+  obtain ⟨C, hBC⟩ := B.exists_isCompl
+  refine ⟨((projectionOnto B C hBC).domRestrict A).toContinuousLinearMap ∘SL p, fun x ↦ ?_⟩
+  simp [hp ⟨x, hB x.2⟩]
+
 omit [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] in
 theorem ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range [T2Space F]
     (f : E →L[𝕜] F) [FiniteDimensional 𝕜 f.range] : f.ker.ClosedComplemented := by