mathlib

67327881 - feat(analysis/normed_space/operator_norm): a few more estimates (#2233)

feat(analysis/normed_space/operator_norm): a few more estimates (#2233) * feat(*): a few more theorems about `unique` and `subsingleton` * Fix compile, fix two non-terminate `simp`s * Update src/topology/metric_space/antilipschitz.lean This lemma will go to another PR * feat(analysis/normed_space/operator_norm): a few more estimates * `le_op_norm_of_le` : `∥x∥ ≤ c → ∥f x∥ ≤ ∥f∥ * c`; * `norm_id` → `norm_id_le`, new `norm_id` assumes `∃ x : E, x ≠ 0` * estimates on the norm of `e : E ≃L[𝕜] F`` and `e.symm`. * rename `(anti)lipschitz_with.to_inverse` to `to_right_inverse` Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>