mpullback_neg

Mathlib.Geometry.Manifold.VectorField.Pullback

URI: https://scilib.ai/kg/mathlib#VectorField.mpullback_neg

English

mpullbackWithin I I' f (−V) s x = − mpullbackWithin I I' f V s x.

Русский

mpullbackWithin I I' f (−V) s x = − mpullbackWithin I I' f V s x.

LaTeX

$$$$ \mathrm{mpullbackWithin}\ I\ I'\ f ( -V)\ s\ x = -\mathrm{mpullbackWithin}\ I\ I'\ f V\ s\ x $$$$

Lean4

theorem mpullback_neg : mpullback I I' f (-V) = -mpullback I I' f V :=
  by
  ext x
  simp [mpullback_apply]

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

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

Разделы

Аффилиация

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