Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-05 20:33 00d86176

View on Github →

feat(analysis/normed_space/inner_product): inner product is continuous, norm squared is smooth (#5600)

Estimated changes

added theorem continuous.inner
added theorem continuous_at.inner
added theorem continuous_on.inner
added theorem deriv_inner_apply
added theorem fderiv_inner_apply
added def fderiv_inner_clm
added theorem fderiv_inner_clm_apply
added theorem filter.tendsto.inner
added theorem has_deriv_at.inner
added theorem has_fderiv_at.inner
added theorem measurable.inner