mfderiv_surjective — Mathlib

English

For x ∈ e.source, the range of mfderiv I I' e x equals the whole tangent space: range = top.

Русский

Для x ∈ области определения множество значений mfderiv охватывает всё касательное пространство: range = top.

LaTeX

$$$\operatorname{range}(mfderiv\,I\,I'\,e\,x) = \top$$$

Lean4

theorem mfderiv_surjective {x : M} (hx : x ∈ e.source) : Function.Surjective (mfderiv I I' e x) :=
  (he.mfderiv hx).surjective

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