contraction_of_isPowMul — Mathlib

English

The simplified contraction lemma: if f is bounded with respect to some seminorm and powMul, then the inequality holds for all x.

Русский

Упрощённая лемма сжатия: если f ограничена относительно некоторой полупрямой нормы и powMul, то неравенство верно для всех x.

LaTeX

$$norm (f x) ≤ norm x$$

Lean4

/-- Given a bounded `f : α →+* β` between seminormed rings, is the seminorm on `β` is
  power-multiplicative, then `f` is a contraction. -/
theorem contraction_of_isPowMul {α β : Type*} [SeminormedRing α] [SeminormedRing β] (hβ : IsPowMul (norm : β → ℝ))
    {f : α →+* β} (hf : f.IsBounded) (x : α) : norm (f x) ≤ norm x :=
  contraction_of_isPowMul_of_boundedWrt (SeminormedRing.toRingSeminorm α) hβ hf x

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