Commit 2021-12-06 06:48 e6ad0f29
View on Github →chore(analysis/inner_product/projections): generalize some lemmas (#10608)
- generalize a few lemmas from
[finite_dimensional 𝕜 ?x]to[complete_space ?x]; - drop unneeded TC assumption in
isometry.tendsto_nhds_iff; - image of a complete set/submodule under an isometry is a complete set/submodule.