contDiff_update — Mathlib

English

The projection onto the i-th coordinate is continuously differentiable of any order on the product space.

Русский

Проекция на i-ю координату является непрерывно дифференцируемой любого порядка на произведение пространств.

LaTeX

$$$\text{ContDiff } 𝕜 k (\text{Pi.single } i : F' i \to \forall i, F' i)$$$

Lean4

theorem contDiff_update [DecidableEq ι] (k : WithTop ℕ∞) (x : ∀ i, F' i) (i : ι) : ContDiff 𝕜 k (update x i) :=
  by
  rw [contDiff_pi]
  intro j
  dsimp [Function.update]
  split_ifs with h
  · subst h
    exact contDiff_id
  · exact contDiff_const

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