Theorems · Theorem · real analysis

hasDerivAtFilter_finCons

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : (i : Fin n.succ) → F' i} {l : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' l ↔
    HasDerivAtFilter φ (φ' 0) l ∧ HasDerivAtFilter φs (fun i => φ' i.succ) l

Defined in

Mathlib.Analysis.Calculus.Deriv.Prod

Cited by

4 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace