mkNormedAddGroupHom_norm_le — Mathlib

English

If a bounded map f : V1 → V2 is constructed from a group homomorphism via a Lipschitz constructor with bound C, then its norm is at most C.

Русский

Если ограниченная отображение f : V1 → V2 получено конструктором на основе гомоморфизма группы сBound C, то его норма не превосходит C.

LaTeX

$$$$ \|\operatorname{ofLipschitz}(f,h)\| \le C $$$$

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
if it is nonnegative. -/
theorem mkNormedAddGroupHom_norm_le (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
    ‖f.mkNormedAddGroupHom C h‖ ≤ C :=
  opNorm_le_bound _ hC h

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