one_le_norm_mul_norm_symm — Mathlib

English

Let e be a continuous linear equivalence between normed spaces with the given ring-isometric structures. Then the product of the operator norms of e and its inverse is at least 1: 1 ≤ ||e|| · ||e^{-1}||.

Русский

Пусть e — непрерывное линейное эквивалентное отображение между нормированными пространства E и F с заданной кольцевой изометрией. Тогда произведение норм операторов e и его обратного отображения не меньше единицы: 1 ≤ ||e|| · ||e^{-1}||.

LaTeX

$$$$1 \\le \\|e\\| \\cdot \\|e^{-1}\\|.$$$$

Lean4

theorem one_le_norm_mul_norm_symm [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :
    1 ≤ ‖(e : E →SL[σ₁₂] F)‖ * ‖(e.symm : F →SL[σ₂₁] E)‖ :=
  by
  rw [mul_comm]
  convert (e.symm : F →SL[σ₂₁] E).opNorm_comp_le (e : E →SL[σ₁₂] F)
  rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]

Похожие утверждения