instCoeFunNonlinearRightInverseForall

English

First step toward Open Mapping: if f: E → F is onto between Banach spaces, then there exists a constant C ≥ 0 such that for every y ∈ F there is x with dist(f x, y) ≤ 1/2 · ‖y‖ and ‖x‖ ≤ C · ‖y‖.

Русский

Первый шаг к теореме об открытом отображении: если f: E → F сюръективно между банаховыми пространствами, существуют C≥0 такие, что для каждого y ∈ F существует x: dist(f x, y) ≤ (1/2)‖y‖ и ‖x‖ ≤ C‖y‖.

LaTeX

$$$$\\exists C \\ge 0, \\forall y, \\exists x, \\ dist(f x, y) \\le \\tfrac{1}{2} \\|y\\| \\ \\land \\ \\|x\\| \\le C \\|y\\|.$$$$

Lean4

instance : CoeFun (NonlinearRightInverse f) fun _ => F → E :=
  ⟨fun fsymm => fsymm.toFun⟩

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