mul_end — Mathlib

English

The product of locally Lipschitz endomorphisms is locally Lipschitz.

Русский

Произведение локально липшицевых эндоморфизмов локально липшицево.

LaTeX

$$$\\forall f,g\\ (hf:\\ LocallyLipschitz f) (hg:\\ LocallyLipschitz g),\\ LocallyLipschitz(f*g)$$$

Lean4

protected theorem mul_end {f g : Function.End α} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz (f * g : Function.End α) :=
  hf.comp hg

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