Submodule.IsCompl.closedComplemented_of_isClosed
theorem Submodule.IsCompl.closedComplemented_of_isClosed :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {p q : Subspace 𝕜 E},
IsCompl p q → IsClosed ↑p → IsClosed ↑q → Submodule.ClosedComplemented p
This theorem, `Submodule.IsCompl.closedComplemented_of_isClosed`, states that for any non-trivially normed field `𝕜`, any normed additive commutative group `E`, for which `𝕜` is a normed space and `E` is a complete space, and any two subspaces `p` and `q` of `𝕜`, if `p` and `q` are complements of each other and the sets of elements in `p` and `q` are both closed, then the subspace `p` is complemented. In other words, there exists a continuous projection from `E` onto `p`.
More concisely: For any non-trivially normed field 𝕜, complete normed additive commutative group E over 𝕜, and closed subspaces p and q of 𝕜 that are complements of each other, there exists a continuous projection from E to p.
|
Submodule.ClosedComplemented.of_isCompl_isClosed
theorem Submodule.ClosedComplemented.of_isCompl_isClosed :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {p q : Subspace 𝕜 E},
IsCompl p q → IsClosed ↑p → IsClosed ↑q → Submodule.ClosedComplemented p
The theorem `Submodule.ClosedComplemented.of_isCompl_isClosed` states that for any two subspaces `p` and `q` of a complete normed space `E` over a nontrivially normed field `𝕜`, if `p` and `q` are complements of each other and both `p` and `q` are closed, then `p` is a complemented submodule. This means there exists a continuous linear projection from `E` onto `p`.
More concisely: If two closed subspaces of a complete normed space over a nontrivially normed field have complementary closures, then one is the continuous linear projection of the other.
|