Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-21 20:35 6c71874b

View on Github →

feat(analysis/normed_space): complemented subspaces (#2738) Define complemented subspaces and prove some basic facts.

Estimated changes

Created src/analysis/normed_space/complemented.lean

added theorem continuous_linear_map.ker_closed_complemented_of_finite_dimensional_range

added theorem subspace.closed_complemented_iff_has_closed_compl

added theorem subspace.closed_complemented_of_closed_compl

added theorem subspace.closed_complemented_of_quotient_finite_dimensional

added theorem subspace.coe_continuous_linear_proj_of_closed_compl'

added theorem subspace.coe_continuous_linear_proj_of_closed_compl

added theorem subspace.coe_prod_equiv_of_closed_compl

added theorem subspace.coe_prod_equiv_of_closed_compl_symm

added def subspace.linear_proj_of_closed_compl

added def subspace.prod_equiv_of_closed_compl

Modified src/linear_algebra/projection.lean

added theorem linear_map.ker_id_sub_eq_of_proj

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.closed_complemented_ker_of_right_inverse

added theorem continuous_linear_map.ker_cod_restrict

added theorem submodule.closed_complemented.has_closed_complement

added def submodule.closed_complemented

added theorem submodule.closed_complemented_bot

added theorem submodule.closed_complemented_top