Theorem isBoundedBilinearMap_inner
Modification history
2025-02-07 10:03
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore(Analysis/InnerProductSpace): split off continuity, convexity of inner product (#21516) …
Modified isBoundedBilinearMap_innerView on Github →