Commit 2021-09-28 06:33 1db626ee

feat(analysis/normed_space/is_bounded_bilinear_map): direct proof of continuity (#9390) Previously is_bounded_bilinear_map.continuous, the continuity of a bounded bilinear map, was deduced from its differentiability and lived in analysis.calculus.fderiv. This PR gives a direct proof so it can live in analysis.normed_space.bounded_linear_maps. Two consequences of this lemma are also moved earlier in the hierarchy:

• continuous_linear_equiv.is_open, the openness of the set of continuous linear equivalences in the space of continuous linear maps, moves from analysis.calculus.fderiv to analysis.normed_space.bounded_linear_maps
• continuous_inner, the continuity of the inner product, moves from analysis.inner_product_space.calculus to analysis.inner_product_space.basic. Previously discussed at https://github.com/leanprover-community/mathlib/pull/4407#pullrequestreview-506198222