norm_contLinear_le — Mathlib

English

The norm of the composition of two continuous affine maps is controlled by the product of norms plus the evaluation at 0 of the outer map.

Русский

Норма композиции двух непрерывных аффинных отображений контролируется произведением норм и значением в 0 внешнего отображения.

LaTeX

$$$$\|f\circ g\| \leq \|f\| \cdot \|g\| + \|f(0)\|.$$$$

Lean4

theorem norm_contLinear_le : ‖f.contLinear‖ ≤ ‖f‖ :=
  le_max_right _ _

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