mkNormedAddGroupHom_norm_le' — Mathlib

English

If a group homomorphism f is bounded by C in norm, then the norm of its normed constructor equals at most max(C,0).

Русский

Если ограничение нормы для f задаётся конструктором с Bound C, то норма скобочной нормированной карты не превосходит max(C,0).

LaTeX

$$$$ \|f.mkNormedAddGroupHom C h\| \le \max\{C,0\} $$$$

Lean4

/-- If a bounded group homomorphism map is constructed from a group homomorphism
via the constructor `AddMonoidHom.mkNormedAddGroupHom`, then its norm is bounded by the bound
given to the constructor or zero if this bound is negative. -/
theorem mkNormedAddGroupHom_norm_le' (f : V₁ →+ V₂) {C : ℝ} (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
    ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0 :=
  opNorm_le_bound _ (le_max_right _ _) fun x => (h x).trans <| by gcongr; apply le_max_left

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