trans — Mathlib

English

The derivative mfderiv I I' e x is surjective for x in the source.

Русский

Производная mfderiv I I' e x сюръектна по отношению к касательному пространству.

LaTeX

$$$\text{mfderiv\_surjective}(I,I',e,x)$$$

Lean4

theorem trans (he' : e'.MDifferentiable I' I'') : (e.trans e').MDifferentiable I I'' :=
  by
  constructor
  · intro x hx
    simp only [mfld_simps] at hx
    exact ((he'.mdifferentiableAt hx.2).comp _ (he.mdifferentiableAt hx.1)).mdifferentiableWithinAt
  · intro x hx
    simp only [mfld_simps] at hx
    exact ((he.symm.mdifferentiableAt hx.2).comp _ (he'.symm.mdifferentiableAt hx.1)).mdifferentiableWithinAt

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