self_of_nhds

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#Filter.Eventually.self_of_nhds

← MathLib Explorer

English

If a predicate holds in a neighborhood of x, then it holds at x.

Русский

Если предикат выполняется в окрестности x, то он выполняется в x.

LaTeX

$$$(\\forall y\\; \\text{(nhds $x$)}\\; p(y)) \\Rightarrow p(x)$$$

Lean4

/-- If a predicate is true in a neighborhood of `x`, then it is true for `x`. -/
theorem self_of_nhds {p : X → Prop} (h : ∀ᶠ y in 𝓝 x, p y) : p x :=
  mem_of_mem_nhds h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru