eventuallyEq_nhds_of_eventuallyEq_nhdsNE

English

Equivalence between nhdsWithin EventuallyEq and nhds EventuallyEq with a predicate describing membership in s.

Русский

Эквивалентность между EventuallyEq в nhdsWithin и в nhds с условием принадлежности к s.

LaTeX

$$$$ ((\\\\nhdsWithin a s).EventuallyEq f g) \\\\iff \\\\mathrm{Eventally} (\\\\lambda x, x \\in s \\rightarrow f x = g x) (\\\\nhds a). $$$$

Lean4

/-- Two functions agree on a neighborhood of `x` if they agree at `x` and in a punctured
neighborhood. -/
theorem eventuallyEq_nhds_of_eventuallyEq_nhdsNE {f g : α → β} {a : α} (h₁ : f =ᶠ[𝓝[≠] a] g) (h₂ : f a = g a) :
    f =ᶠ[𝓝 a] g := by
  filter_upwards [eventually_nhdsWithin_iff.1 h₁]
  intro x hx
  by_cases h₂x : x = a
  · simp [h₂x, h₂]
  · tauto

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