contMDiff_of_contMDiff_inr — Mathlib

English

Sum.map f g is ContMDiff iff both f and g are ContMDiff.

Русский

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_of_contMDiff_inr {g : M' → N'} (h : ContMDiff I J n ((@Sum.inr N N') ∘ g)) : ContMDiff I J n g :=
  by
  nontriviality N'
  inhabit N'
  let aux : N ⊕ N' → N' := Sum.elim (fun _ ↦ inhabited_h.default) (@id N')
  have : aux ∘ (@Sum.inr N N') ∘ g = g := by ext; simp [aux]
  rw [← this]
  rw [← contMDiffOn_univ] at h ⊢
  apply ((contMDiff_const.sumElim contMDiff_id).contMDiffOn (s := Sum.inr '' univ)).comp h
  intro x _hx
  rw [mem_preimage, Function.comp_apply]
  use g x, trivial

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