self_of_nhdsWithin — Mathlib

English

If eventually p holds along nhdsWithin a s, and a ∈ s, then p(a) holds.

Русский

Если почти всегда выполняется p вдоль nhdsWithin a s, и a∈s, то p(a) выполняется.

LaTeX

$$$ \forall {p:\, \alpha\to \mathrm{Prop}},\ (h:\forall^\infty y\in \mathcal{N}_s(a),\ p(y))\land (ha:\ a\in s)\Rightarrow p(a) $$$

Lean4

theorem self_of_nhdsWithin {p : α → Prop} {s : Set α} {x : α} (h : ∀ᶠ y in 𝓝[s] x, p y) (hx : x ∈ s) : p x :=
  mem_of_mem_nhdsWithin hx h

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