hasGradientAtFilter_iff — Mathlib

English

Let f₀,f₁ : F → 𝕜, x ∈ F and L be a filter. If f₀ =ᶠ[L] f₁ and f₀(x) = f₁(x) and f₀' = f₁', then HasGradientAtFilter f₀ f₀' x L holds iff HasGradientAtFilter f₁ f₁' x L.

Русский

Пусть f₀, f₁ : F → 𝕜, x ∈ F и фильтр L. Если f₀ равна f₁ вдоль L и значения в x совпадают, и градиенты совпадают, то характеристика градиента вдоль фильтра сохраняется взаимно.

LaTeX

$$$\text{HasGradientAtFilter}(f_0,f_0',x,L) \iff \text{HasGradientAtFilter}(f_1,f_1',x,L)$ при $f_0 =^L f_1$, $f_0(x)=f_1(x)$ и $f_0'=f_1'$$$

Lean4

theorem hasGradientAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : f₀' = f₁') :
    HasGradientAtFilter f₀ f₀' x L ↔ HasGradientAtFilter f₁ f₁' x L :=
  h₀.hasFDerivAtFilter_iff hx (by simp [h₁])

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