ker_mfderiv_eq_bot

Mathlib.Geometry.Manifold.MFDeriv.Atlas

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

English

For x ∈ e.source, the kernel of mfderiv I I' e x is {0}.

Русский

Для x ∈ области определения ядро mfderiv I I' e x состоит из нуля.

LaTeX

$$$\ker(mfderiv I I' e x) = \{0\}$$$

Lean4

theorem ker_mfderiv_eq_bot {x : M} (hx : x ∈ e.source) : LinearMap.ker (mfderiv I I' e x) = ⊥ :=
  (he.mfderiv hx).toLinearEquiv.ker

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

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

Разделы

Аффилиация

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