congr — Mathlib

English

AHasLineDerivAt f f' at x in direction v is equivalent to the limit of the difference quotient along the line t ↦ x + t v as t → 0, with t restricted appropriately.

Русский

Утверждение о наличии линейной производной вдоль направления v в точке x эквивалентно пределу разности при движении вдоль линии x + t v при t → 0.

LaTeX

$$$\text{HasLineDerivAt}_{\mathbb{k}}(f,f',x,v) \iff \mathrm{Tendsto}(t \mapsto t^{-1}(f(x+t v)-f(x)), \cdots, f')$$$

Lean4

theorem congr (h : LineDifferentiableWithinAt 𝕜 f s x v) (ht : ∀ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) :
    LineDifferentiableWithinAt 𝕜 f₁ s x v :=
  LineDifferentiableWithinAt.congr_mono h ht hx (Subset.refl _)

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