Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-18 08:44 f68c936c

View on Github →

feat(analysis/normed_space/real_inner_product): orthogonal subspace lemmas (#4152) Add a few more lemmas about submodule.orthogonal.

Estimated changes

Modified src/analysis/normed_space/real_inner_product.lean

added theorem submodule.findim_add_inf_findim_orthogonal

added theorem submodule.orthogonal_le

added theorem submodule.sup_orthogonal_inf_of_is_complete