normNoninc_iff_norm_le_one — Mathlib

English

The identity map id_V is NormNoninc, i.e., it does not increase norms.

Русский

Тождественное отображение id_V не увеличивает норму: NormNoninc.

LaTeX

$$$\\text{id}_V.NormNoninc$$$

Lean4

theorem normNoninc_iff_norm_le_one : f.NormNoninc ↔ ‖f‖ ≤ 1 :=
  by
  refine ⟨fun h => ?_, fun h => fun v => ?_⟩
  · refine opNorm_le_bound _ zero_le_one fun v => ?_
    simpa [one_mul] using h v
  · simpa using le_of_opNorm_le f h v

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