exists_mem — Mathlib

English

Let f be a filter on a set α and p : α → Prop. If p holds eventually with respect to f, then there exists a set V ∈ f such that p(y) holds for all y ∈ V.

Русский

Пусть f — фильтр на множество α и p : α → Prop. Если p выполняется часто относительно f, то существует множество V ∈ f такое, что для каждого y ∈ V верно p(y).

LaTeX

$$$ (\forall^\infty x \in f,\ p\ x) \rightarrow \exists V \in f,\ \forall y \in V,\ p\ y $$$

Lean4

theorem exists_mem {p : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) : ∃ v ∈ f, ∀ y ∈ v, p y :=
  eventually_iff_exists_mem.1 hp

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