Complemented subspaces of normed vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
p of a topological module
R is called complemented if there exists
a continuous linear projection
f : E →ₗ[R] p,
∀ x : p, f x = x. We prove that for
a closed subspace of a normed space this condition is equivalent to existence of a closed
q such that
p ⊓ q = ⊥,
p ⊔ q = ⊤. We also prove that a subspace of finite codimension
is always a complemented subspace.
complemented subspace, normed vector space
f : E →L[R] F and
g : E →L[R] G are two surjective linear maps and
their kernels are complement of each other, then
x ↦ (f x, g x) defines
a linear equivalence
E ≃L[R] F × G.
- f.equiv_prod_of_surjective_of_is_compl g hf hg hfg = (↑f.equiv_prod_of_surjective_of_is_compl ↑g hf hg hfg).to_continuous_linear_equiv_of_continuous _
q is a closed complement of a closed subspace
p × q is continuously
- p.prod_equiv_of_closed_compl q h hp hq = (submodule.prod_equiv_of_is_compl p q h).to_continuous_linear_equiv_of_continuous _
Projection to a closed submodule along a closed complement.
- p.linear_proj_of_closed_compl q h hp hq = (continuous_linear_map.fst 𝕜 ↥p ↥q).comp ↑((p.prod_equiv_of_closed_compl q h hp hq).symm)