mathlib3

8438172d - chore(analysis/inner_product/projections): generalize some lemmas (#10608)

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.