mpullback_zero

Mathlib.Geometry.Manifold.VectorField.Pullback

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

English

In the general setting, mpullback I I f V equals pullback 𝕜 f V.

Русский

В общем случае mpullback I I f V равен pullback 𝕜 f V.

LaTeX

$$$$ \mathrm{mpullback}\ I\ I' f V = \mathrm{pullback}\ 𝕜 f V $$$$

Lean4

@[simp]
theorem mpullback_zero : mpullback I I' f 0 = 0 := by simp [← mpullbackWithin_univ]

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

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

Разделы

Аффилиация

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