Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-28 03:34 67327881

View on Github →

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 simps
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

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

deleted theorem continuous_linear_equiv.antilipschitz

deleted theorem continuous_linear_equiv.lipschitz

added theorem continuous_linear_equiv.norm_pos

added theorem continuous_linear_equiv.norm_symm_pos

added theorem continuous_linear_equiv.one_le_norm_mul_norm_symm

added theorem continuous_linear_equiv.subsingleton_or_nnnorm_symm_pos

added theorem continuous_linear_equiv.subsingleton_or_norm_symm_pos

modified theorem continuous_linear_equiv.uniform_embedding

added theorem continuous_linear_map.le_op_norm_of_le

modified theorem continuous_linear_map.norm_id

added theorem continuous_linear_map.norm_id_le

modified theorem continuous_linear_map.op_norm_comp_le

Modified src/topology/metric_space/antilipschitz.lean

deleted theorem antilipschitz_with.to_inverse

added theorem antilipschitz_with.to_right_inverse

deleted theorem lipschitz_with.to_inverse

added theorem lipschitz_with.to_right_inverse