-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span #15481
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(EDIT: mistake)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
/-- Any finite subset of a orthonormal family is an `orthonormal_basis` for its span. -/ | ||
protected def span {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') : | ||
orthonormal_basis s 𝕜 (span 𝕜 (s.image v' : set E)) := | ||
let |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For consistency, could you write the proof in the same way as in basis.span
, using orthonormal_basis.mk
?
This PR/issue depends on: |
Please merge master and then merge yourself. Thanks! bors + |
Did you mean "r+"? |
bors d+ |
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…basis of its span (#15481) We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice
Pull request successfully merged into master. Build succeeded: |
…basis of its span (leanprover-community#15481) We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice
…basis of its span (#15481) We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice
…basis of its span (#15481) We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice
We actually prove this for finite sub-families of a generic orthonormal basis because this is easier to use in practice
linear_equiv.of_eq
as alinear_isometry_equiv
#15471