tangentMapWithin_univ — Mathlib

English

The tangent map within the universal set equals the tangent map on the whole space.

Русский

Касательная карта внутри множества-univ равна касательной карте на всём пространстве.

LaTeX

$$$$tangentMapWithin I I' f univ = tangentMap I I' f$$$$

Lean4

theorem tangentMapWithin_univ : tangentMapWithin I I' f univ = tangentMap I I' f :=
  by
  ext p : 1
  simp only [tangentMapWithin, tangentMap, mfld_simps]

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