affine_subspace): more `mem_map` lemmas (#16378)

Commit

3 years ago

feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378) Add two more lemmas about membership of an affine subspace given by `affine_subspace.map`.

Author

jsm28

Parents

a0ae2165

mathlib 7afe23e0 - feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378)

mathlib
7afe23e0 - feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378)