equivTangentBundleProd_eq_tangentMap_prod_tangentMap

English

A composition of tangents and maps preserves continuity: the tangent map on a product is continuous when inputs vary smoothly.

Русский

Сохранение непрерывности через касательное отображение и произведение.

LaTeX

$$$\forall f : M \to M',\; ContMDiffMap.mdifferentiable f \Rightarrow Continuous (tangentMap (I.prod I') (M \times M')) $$$

Lean4

theorem equivTangentBundleProd_eq_tangentMap_prod_tangentMap :
    equivTangentBundleProd I M I' M' = fun (p : TangentBundle (I.prod I') (M × M')) ↦
      (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p) :=
  by simp only [tangentMap_prodFst, tangentMap_prodSnd]; rfl

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