mkNormedAddGroupHom' — Mathlib

English

Associate to a group homomorphism a bounded homomorphism using ℝ≥0 as a bound.

Русский

Ассоциируемому гомоморфизму группы задаём ограниченный по норме гомоморфизм с границей в ℝ≥0.

LaTeX

$$$\\mathrm{mkNormedAddGroupHom}'(f, C, h_C)$$$

Lean4

/-- Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

See `AddMonoidHom.mkNormedAddGroupHom` for a version that uses `ℝ` for the bound. -/
def mkNormedAddGroupHom' (f : V →+ W) (C : ℝ≥0) (hC : ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊) : NormedAddGroupHom V W :=
  { f with bound' := ⟨C, hC⟩ }

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