congr — Mathlib

English

If HasFTaylorSeriesUpToOn n f p s and h₁ : ∀ x ∈ s, f₁ x = f x, then HasFTaylorSeriesUpToOn n f₁ p s.

Русский

Если HasFTaylorSeriesUpToOn n f p s и f₁ совпадает с f на s, то HasFTaylorSeriesUpToOn n f₁ p s.

LaTeX

$$HasFTaylorSeriesUpToOn\ n f\ p\ s → (∀ x ∈ s, f₁ x = f x) → HasFTaylorSeriesUpToOn n f₁ p s$$

Lean4

/-- If two functions coincide on a set `s`, then a Taylor series for the first one is as well a
Taylor series for the second one. -/
theorem congr (h : HasFTaylorSeriesUpToOn n f p s) (h₁ : ∀ x ∈ s, f₁ x = f x) : HasFTaylorSeriesUpToOn n f₁ p s :=
  by
  refine ⟨fun x hx => ?_, h.fderivWithin, h.cont⟩
  rw [h₁ x hx]
  exact h.zero_eq x hx

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