finite_dimension): a finite dimensional affine subspace is closed (#13440)

Commit

3 years ago

feat(analysis/normed_space/finite_dimension): a finite dimensional affine subspace is closed (#13440)

Author

urkud

Parents