sumMap

Mathlib.Geometry.Manifold.ContMDiff.Constructions

URI: https://scilib.ai/kg/mathlib#ContMDiff.sumMap

← MathLib Explorer

English

If Sum.inl f is ContMDiff, then f itself is ContMDiff.

Русский

Если Sum.inl f гладко, тогда f гладко.

LaTeX

$$$ \text{contMDiff_of_contMDiff_inl} : \ (h : ContMDiff I J n (Sum.inl \circ f)) \Rightarrow \ ContMDiff I J n f $$$

Lean4

theorem sumMap {f : M → N} {g : M' → N'} (hf : ContMDiff I J n f) (hg : ContMDiff I J n g) :
    ContMDiff I J n (Sum.map f g) :=
  ContMDiff.sumElim (ContMDiff.inl.comp hf) (ContMDiff.inr.comp hg)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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