mkNormedAddGroupHom — Mathlib

English

Given a group homomorphism f: V→W and a constant C with a norm bound ∥f v∥ ≤ C∥v∥, define a bounded NormedAddGroupHom with bound C.

Русский

Дано гомоморфизм f: V→W и константа C, удовлетворяющая ограничению по норме ∥f v∥ ≤ C∥v∥; образуется ограниченная NormedAddGroupHom.

LaTeX

$$$\\mathrm{mkNormedAddGroupHom}(f, C, h)$ где $h(v): \\|f v\\| ≤ C \\|v\\|$$$

Lean4

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

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

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