injOn — Mathlib

English

If f is approximated by a linear surrogate on s with bound c, and either E is subsingleton or c < 1/N, then f is injective on s.

Русский

Если функция f аппроксимируется на s линейной подстановкой с ограничением c и либо E сколь угодно тривиально, либо c < 1/N, то f инъективна на s.

LaTeX

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

Lean4

protected theorem injOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
    InjOn f s :=
  injOn_iff_injective.2 <| hf.injective hc

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