norm_compContinuous_le — Mathlib

English

Precomposition by a continuous map yields a bounded continuous map whose norm does not exceed the original.

Русский

Пре-композиция непрерывной картой дает ограниченную непрерывную карту с нормой не превышающей исходную.

LaTeX

$$$‖f.compContinuous g‖ ≤ ‖f‖$$$

Lean4

theorem norm_compContinuous_le [TopologicalSpace γ] (f : α →ᵇ β) (g : C(γ, α)) : ‖f.compContinuous g‖ ≤ ‖f‖ :=
  ((lipschitz_compContinuous g).dist_le_mul f 0).trans <| by rw [NNReal.coe_one, one_mul, dist_zero_right]

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