eventually_ne_nhdsWithin — Mathlib

English

There exists a neighborhood around x in the punctured neighborhood where e is not constant; i.e., e(y) ≠ e(x) for y ≠ x sufficiently close to x in e.source.

Русский

Существует окрестность вокруг x в punctured-окрестности, в которой e не константна; т.е. значения различаются близко к x.

LaTeX

$$$\forall x' \in 𝓝[\setminus{ x }] x: e(x') \neq e(x)$$$

Lean4

theorem eventually_ne_nhdsWithin {x} (hx : x ∈ e.source) : ∀ᶠ x' in 𝓝[≠] x, e x' ≠ e x :=
  eventually_nhdsWithin_iff.2 <|
    (e.eventually_left_inverse hx).mono fun x' hx' => mt fun h => by rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']

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