mpullbackWithin_zero

Mathlib.Geometry.Manifold.VectorField.Pullback

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mpullbackWithin_zero : mpullbackWithin I I' f 0 s = 0 :=
  by
  ext x
  simp [mpullbackWithin_apply]

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

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

Разделы

Аффилиация

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