Commit 2020-12-30 15:51 c82be35d

View on Github →

feat(analysis/normed_space/inner_product): orthogonal complement lemmas (#5474) The orthogonal complement of a subspace is closed. The orthogonal complement of the orthogonal complement of a complete subspace is itself.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added def inner_right

added theorem inner_right_apply

added theorem inner_right_coe

added theorem orthogonal_eq_inter

added theorem submodule.exists_sum_mem_mem_orthogonal

added theorem submodule.is_closed_orthogonal

added theorem submodule.orthogonal_orthogonal

added theorem submodule.sup_orthogonal_of_complete_space