English
If a bounded linear map f: E →L[𝕜] F is bijective, then it is a unit in the operator ring; equivalently, there exists an inverse that is also a bounded linear map.
Русский
Если отображение f: E →L[𝕜] F биективно, то оно является единицей в кольце линейных операторов; эквивалентно существованию обратного отображения, которое тоже ограничено линейно.
LaTeX
$$$f \\text{ is a unit } \\iff f \\text{ is bijective}$$$
Lean4
/-- If `f : E →L[𝕜] F` is injective with closed range (and `E` and `F` are Banach spaces),
`f` is anti-Lipschitz. -/
theorem antilipschitz_of_injective_of_isClosed_range (f : E →L[𝕜] F) (hf : Injective f) (hf' : IsClosed (Set.range f)) :
∃ K, AntilipschitzWith K f :=
by
let S : (LinearMap.range f) →L[𝕜] E := (f.equivRange hf hf').symm
use ⟨S.opNorm, S.opNorm_nonneg⟩
apply ContinuousLinearMap.antilipschitz_of_bound
intro x
calc
‖x‖
_ = ‖S ⟨f x, by simp⟩‖ := by simp [S]
_ ≤ S.opNorm * ‖f x‖ := le_opNorm S ⟨f x, by simp⟩
