nonlinearRightInverseOfSurjective_nnnorm_pos

English

For an injective bounded linear map f: E →L[𝕜] F between Banach spaces, the following are equivalent: (i) range(f) is closed; (ii) there exists K > 0 such that f is K-antilipschitz, i.e., ∥x−y∥ ≤ K∥f(x)−f(y)∥. In particular, closed range iff antilipschitz.

Русский

Для инъективного ограниченного линейного отображения f: E →L[𝕜] F между банаховыми пространствами эквивалентны условия: (i) образ замкнут; (ii) существует K>0: ∥x−y∥ ≤ K∥f(x)−f(y)∥. Следовательно, замкнутость диапазона эквивалентна антиллипшичности.

LaTeX

$$$\\text{IsClosed}(\\operatorname{range} f) \\iff \\exists K>0, \\; \\text{AntilipschitzWith}(K,f)$$$

Lean4

theorem nonlinearRightInverseOfSurjective_nnnorm_pos (f : E →SL[σ] F) (hsurj : LinearMap.range f = ⊤) :
    0 < (nonlinearRightInverseOfSurjective f hsurj).nnnorm :=
  by
  rw [nonlinearRightInverseOfSurjective]
  exact Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)

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