bound — Mathlib

English

There exists a bound C for a linear map given continuous nature, i.e., ∃C, ∀x, ‖f x‖ ≤ C‖x‖.

Русский

Существование границы C для линейного отображения f при условии его непрерывности.

LaTeX

$$$\exists C>0, \forall x, \|f x\| ≤ C \|x\|$$$

Lean4

theorem bound [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : ∃ C, 0 < C ∧ ∀ x : E, ‖f x‖ ≤ C * ‖x‖ :=
  SemilinearMapClass.bound_of_continuous f f.2

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