eventually_mem — Mathlib

English

If f is continuous at x and s is a set with s ∈ 𝓝(f(x)), then f(y) ∈ s for all y sufficiently near x (i.e., eventually in 𝓝 x).

Русский

Если f непрерывна в x и s ∈ 𝓝(f(x)), то f(y) ∈ s для всех y достаточно близко к x (то естьEventually в 𝓝 x).

LaTeX

$$$\\mathrm{ContinuousAt}(f, x) \\Rightarrow \\big( s \\in 𝓝(f(x)) \\Rightarrow \\forall^\\! y \\in 𝓝(x), f(y) \\in s \\big)$$$

Lean4

/-- If `f x ∈ s ∈ 𝓝 (f x)` for continuous `f`, then `f y ∈ s` near `x`.

This is essentially `Filter.Tendsto.eventually_mem`, but infers in more cases when applied. -/
theorem eventually_mem {f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y} (hs : s ∈ 𝓝 (f x)) :
    ∀ᶠ y in 𝓝 x, f y ∈ s :=
  hf hs

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