range_mfderiv_eq_top

Mathlib.Geometry.Manifold.MFDeriv.Atlas

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

English

For x ∈ e.source, the range of mfderiv I I' e x is univ (the whole space).

Русский

Для x ∈ области определения диапазон mfderiv I I' e x покрывает всю область.

LaTeX

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

Lean4

theorem range_mfderiv_eq_top {x : M} (hx : x ∈ e.source) : LinearMap.range (mfderiv I I' e x) = ⊤ :=
  (he.mfderiv hx).toLinearEquiv.range

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

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

Разделы

Аффилиация

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