norm_image_sub_le — Mathlib

English

The norm of the image bound is controlled by the bound on f and the norm of the difference m1−m2.

Русский

Норма изображения ограничена нормой f и нормой разности м1−м2.

LaTeX

$$$\|f m_1 - f m_2\| \le \|f\| \cdot \|m_1 - m_2\| \cdot \text{(product of norms of other components)}$$$

Lean4

/-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`,
less precise version.
For a more precise but less usable version, see `norm_image_sub_le'`.
The bound is `‖f m - f m'‖ ≤ ‖f‖ * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`. -/
theorem norm_image_sub_le (f : E [⋀^ι]→L[𝕜] F) (m₁ m₂ : ι → E) :
    ‖f m₁ - f m₂‖ ≤ ‖f‖ * (Fintype.card ι) * (max ‖m₁‖ ‖m₂‖) ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ :=
  f.1.norm_image_sub_le m₁ m₂

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