feat: isEmbedding_subtypeL (leanprover-community#40716)

This PR was automatically created from PR leanprover-community#39100 by @ADedecker via a [review comment](leanprover-community#39100 (comment)) by @ADedecker.

Co-authored-by: ADedecker <48656793+ADedecker@users.noreply.github.com>

Author: 2 people

Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean

@@ -58,6 +58,14 @@ alias coe_subtypeL' := coe_subtypeL
 
 theorem subtypeL_apply (p : Submodule R M) (x : p) : p.subtypeL x = x := by simp
 
+theorem isEmbedding_subtype (p : Submodule R M) : Topology.IsEmbedding p.subtype := .subtypeVal
+theorem isEmbedding_subtypeL (p : Submodule R M) : Topology.IsEmbedding p.subtypeL := .subtypeVal
+
+theorem isClosedEmbedding_subtype (p : Submodule R M) (hp : IsClosed (p : Set M)) :
+    Topology.IsClosedEmbedding p.subtype := .subtypeVal hp
+theorem isClosedEmbedding_subtypeL (p : Submodule R M) (hp : IsClosed (p : Set M)) :
+    Topology.IsClosedEmbedding p.subtypeL := .subtypeVal hp
+
 @[deprecated range_subtype (since := "2026-05-06")]
 theorem range_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).range = p :=
   Submodule.range_subtype _