instInhabitedNonlinearRightInverseToContinuousLinearMap

English

If an affine map f: P → Q between normed spaces is continuous and surjective, then f is an open map.

Русский

Если аффинное отображение f: P → Q между нормированными пространствами непрерывно и сюръективно, то оно открытое.

LaTeX

$$$$f \\text{ is open}.$$$$

Lean4

noncomputable instance [RingHomInvPair σ' σ] (f : E ≃SL[σ] F) :
    Inhabited (ContinuousLinearMap.NonlinearRightInverse (f : E →SL[σ] F)) :=
  ⟨f.toNonlinearRightInverse⟩

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