range_mfderiv_eq_univ

Mathlib.Geometry.Manifold.MFDeriv.Atlas

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ

English

Another form of surjectivity: the range is univ.

Русский

Ещё одна форма утверждения сюръективности: диапазон равен univ.

LaTeX

$$$\operatorname{range}(mfderiv I I' e x) = \mathsf{univ}$$$

Lean4

theorem range_mfderiv_eq_univ {x : M} (hx : x ∈ e.source) : range (mfderiv I I' e x) = univ :=
  (he.mfderiv_surjective hx).range_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru