contMDiff_of_contMDiff_inl — Mathlib

English

If Sum.inr g is ContMDiff, then g itself is ContMDiff.

Русский

Если Sum.inr g гладко, тогда g гладко.

LaTeX

$$$ \text{contMDiff_of_contMDiff_inr} : \ (h : ContMDiff I J n (Sum.inr \circ g)) \Rightarrow \ ContMDiff I J n g $$$

Lean4

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

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