differentiableOn_apply — Mathlib

English

Differentiability on a set is equivalent to all coordinates being differentiable on that set.

Русский

Дифференцируемость на множестве эквивалентна дифференцируемости всех координат на этом множестве.

LaTeX

$$$\\text{DifferentiableWithinAt } Φ s x \\iff \\forall i, \\text{DifferentiableWithinAt } Φ_i s x.$$$

Lean4

@[fun_prop]
theorem differentiableOn_apply (i : ι) (s' : Set (∀ i, F' i)) :
    DifferentiableOn (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) s' :=
  by
  have h := ((differentiableOn_pi (𝕜 := 𝕜) (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (s := s'))).1
  apply h; apply differentiableOn_id

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