completeSpace_range_clm — Mathlib

English

A continuous linear map f is bijective if and only if range f is dense in F and there exists an antilipschitz bound.

Русский

Пусть линейное отображение f непрерывно; тогда биективно оно тогда и только тогда, когда образ инъективен и диапазон плотен в F и существует антилипшицево ограничение.

LaTeX

$$$Bijective(f) \iff (\overline{\operatorname{range} f} = \top) \land \exists c, AntilipschitzWith c f$$$

Lean4

theorem _root_.AntilipschitzWith.completeSpace_range_clm {f : E →SL[σ] F} {c : ℝ≥0} (hf : AntilipschitzWith c f) :
    CompleteSpace (LinearMap.range f) :=
  IsClosed.completeSpace_coe (hs := hf.isClosed_range f.uniformContinuous)

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