Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dense.eq_of_sub_mem_orthogonal

Modification history

2022-11-12 02:18

src/analysis/inner_product_space/projection.lean

feat(analysis/inner_product_space): ext lemmas for dense subspaces (#17450)

Added dense.eq_of_sub_mem_orthogonal View on Github →