eventually_nhdsSet_iff_exists — Mathlib

English

(∖forall) ∀ᶠ x in nhdsSet s, p x iff ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x.

Русский

Положено: существует открытое множество t, содержащее s, такое что ∀ x ∈ t, p x выполняется (производится eventually).

LaTeX

$$$(\\forallᶠ x \\in nhdsSet s, p x) \\iff \\exists t, IsOpen t ∧ s ⊆ t ∧ ∀ x, x ∈ t → p x$$$

Lean4

/-- A proposition is true on a set neighborhood of `s` iff it is true on a larger open set -/
theorem eventually_nhdsSet_iff_exists {p : X → Prop} : (∀ᶠ x in 𝓝ˢ s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x, x ∈ t → p x :=
  mem_nhdsSet_iff_exists

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