tangentBundle_proj_preimage — Mathlib

English

If a set s has the unique differential property in M, then its preimage under the projection from the tangent bundle also has the unique differential property in the tangent bundle.

Русский

Если множество s имеет уникальное дифференциальное свойство в M, то его предобраз по проекции касательного расхождения также имеет это свойство в касательном расхождении.

LaTeX

$$$UniqueMDiffOn\\ I\\ tangent\\ (\\pi^{E(TangentSpace I)}^{-1}(s))$ given $hs : UniqueMDiffOn I s$.$$

Lean4

/-- The preimage under the projection from the tangent bundle of a set with unique differential in
the basis also has unique differential. -/
theorem tangentBundle_proj_preimage {s : Set M} (hs : UniqueMDiffOn I s) :
    UniqueMDiffOn I.tangent (π E(TangentSpace I) ⁻¹' s) :=
  hs.bundle_preimage _

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