contMDiff_sum_map — Mathlib

English

Another formulation: ContMDiff of Sum.map f g is equivalent to ContMDiff of f and g.

Русский

Еще одна формулировка: гладкость Sum.map f g эквивалентна гладкости f и g.

LaTeX

$$$ ContMDiff I J n (Sum.map f g) \iff ContMDiff I J n f \land ContMDiff I J n g $$$

Lean4

theorem contMDiff_sum_map {f : M → N} {g : M' → N'} :
    ContMDiff I J n (Sum.map f g) ↔ ContMDiff I J n f ∧ ContMDiff I J n g :=
  ⟨fun h ↦ ⟨contMDiff_of_contMDiff_inl (h.comp ContMDiff.inl), contMDiff_of_contMDiff_inr (h.comp ContMDiff.inr)⟩,
    fun h ↦ ContMDiff.sumMap h.1 h.2⟩

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