congr_of_eventuallyEq — Mathlib

English

If HasGradientWithinAt f f' s x holds and f₁ coincides with f on t ⊆ s while f₁ x = f x, then HasGradientWithinAt f₁ f' t x.

Русский

Если существую градиент внутри множества s, а функция f₁ совпадает с f на подмножества t, причём t ⊆ s и x ∈ t, то сохраняется градиент внутри t.

LaTeX

$$HasGradientWithinAt f f' s x → (∀ x ∈ t, f₁ x = f x) → t ⊆ s → HasGradientWithinAt f₁ f' t x$$

Lean4

theorem congr_of_eventuallyEq (h : HasGradientAtFilter f f' x L) (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) :
    HasGradientAtFilter f₁ f' x L := by rwa [hL.hasGradientAtFilter_iff hx rfl]

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