mem_finsupport — Mathlib

English

If each g_i is ContDiffAt at x0 on tsupport, then the finsum is ContDiffAt at x0.

Русский

Если каждый g_i гладко дифференцируем в x0 на tsupport, то сумма finsum гладко дифференцируема в x0.

LaTeX

$$$\forall x_0, (\forall i, x_0 \in tsupport(f_i) \Rightarrow ContDiffAt \; (g_i)\ x_0) \Rightarrow ContDiffAt\; (\lambda x. \sum^\infty_i f_i(x) g_i(x))\ x_0$$$

Lean4

@[simp]
theorem mem_finsupport {i : ι} : i ∈ ρ.finsupport x₀ ↔ i ∈ support fun i ↦ ρ i x₀ :=
  ρ.toPartitionOfUnity.mem_finsupport x₀

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