# mathlibdocumentation

analysis.normed_space.complemented

# Complemented subspaces of normed vector spaces

A submodule p of a topological module E over 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 subspace q such that p ⊓ q = ⊥, p ⊔ q = ⊤. We also prove that a subspace of finite codimension is always a complemented subspace.

## Tags

complemented subspace, normed vector space

theorem continuous_linear_map.ker_closed_complemented_of_finite_dimensional_range {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) [ (f.range)] :

def continuous_linear_map.equiv_prod_of_surjective_of_is_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] [complete_space (F × G)] (f : E →L[𝕜] F) (g : E →L[𝕜] G) :
f.range = g.range = g.ker(E ≃L[𝕜] F × G)

If 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.

Equations
• hg hfg =
@[simp]
theorem continuous_linear_map.coe_equiv_prod_of_surjective_of_is_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] [complete_space (F × G)] {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : f.range = ) (hg : g.range = ) (hfg : g.ker) :
hg hfg) = (f.prod g)

@[simp]
theorem continuous_linear_map.equiv_prod_of_surjective_of_is_compl_to_linear_equiv {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] [complete_space (F × G)] {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : f.range = ) (hg : g.range = ) (hfg : g.ker) :
hg hfg).to_linear_equiv = hfg

@[simp]
theorem continuous_linear_map.equiv_prod_of_surjective_of_is_compl_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {G : Type u_4} [normed_group G] [ G] [complete_space (F × G)] {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : f.range = ) (hg : g.range = ) (hfg : g.ker) (x : E) :
hg hfg) x = (f x, g x)

def subspace.prod_equiv_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (p q : E) :
q((p × q) ≃L[𝕜] E)

If q is a closed complement of a closed subspace p, then p × q is continuously isomorphic to E.

Equations
def subspace.linear_proj_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (p q : E) :
q(E →L[𝕜] p)

Projection to a closed submodule along a closed complement.

Equations
@[simp]
theorem subspace.coe_prod_equiv_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p q : E} (h : q) (hp : is_closed p) (hq : is_closed q) :
hp hq) =

@[simp]
theorem subspace.coe_prod_equiv_of_closed_compl_symm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p q : E} (h : q) (hp : is_closed p) (hq : is_closed q) :
h hp hq).symm) = h).symm)

@[simp]
theorem subspace.coe_continuous_linear_proj_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p q : E} (h : q) (hp : is_closed p) (hq : is_closed q) :
hp hq) =

@[simp]
theorem subspace.coe_continuous_linear_proj_of_closed_compl' {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p q : E} (h : q) (hp : is_closed p) (hq : is_closed q) :
hp hq) =

theorem subspace.closed_complemented_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p q : E} :
q

theorem subspace.closed_complemented_iff_has_closed_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p : E} :
∃ (q : E) (hq : , q

theorem subspace.closed_complemented_of_quotient_finite_dimensional {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {p : E}  :