tangentMapWithin_proj — Mathlib

English

The projection of the tangent map within s equals the base map composed with the projection.

Русский

Проекция касательной карты внутри s равна композиции касательной карты с проекцией базового пространства.

LaTeX

$$$$ (tangentMapWithin I I' f s p).proj = f p.proj $$$$

Lean4

@[simp, mfld_simps]
theorem tangentMapWithin_proj {p : TangentBundle I M} : (tangentMapWithin I I' f s p).proj = f p.proj :=
  rfl

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