injective — Mathlib

English

Let f: E → F be approximated on a set s by a continuous linear isomorphism f' with bound c ≥ 0. If E is not a singleton or c is strictly smaller than 1/N, then the restriction of f to s is injective.

Русский

Пусть f: E → F аппроксимируется на множествах s некоторым непрерывным линейным отображением-изоморфизмом f' с константой аппроксимации c ≥ 0. Если E не тождественно сколь угодно тривиальная (неединственный элемент) или c < N⁻¹, то ограничение f на s инъективно.

LaTeX

$$$\text{ApproximatesLinearOn } f (f' : E \to L[𝕜] F)\ s\ c \;\to\ (Subsingleton E \;\lor\; c < N^{-1})\;\to\; Injective (s.restrict f)$$$

Lean4

protected theorem injective (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
    Injective (s.restrict f) :=
  (hf.antilipschitz hc).injective

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