Commit 2021-04-17 09:45 e9a11f6e

View on Github →

feat(analysis/normed_space/operator_norm): generalize to seminormed space (#7202) This PR is part of a series of PRs to have seminormed stuff in mathlib. We generalize here operator_norm to semi_normed_space. I didn't do anything complicated, essentially I only generalized what works out of the box, without trying to modify the proofs that don't work.

Estimated changes

Modified src/analysis/analytic/linear.lean

Modified src/analysis/normed_space/extend.lean

modified theorem continuous_linear_map.extend_to_𝕜'_apply

modified theorem norm_bound

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.norm_id_of_nontrivial_seminorm

modified theorem continuous_linear_map.op_norm_comp_linear_isometry_equiv

modified theorem continuous_linear_map.op_norm_smul_le

added theorem continuous_linear_map.op_norm_zero

modified theorem linear_equiv.uniform_embedding

modified theorem linear_map.bound_of_shell

added theorem linear_map.bound_of_shell_semi_normed

added theorem norm_image_of_norm_zero

Modified src/data/complex/is_R_or_C.lean