exists — Mathlib

English

If f is nontrivial and p holds eventually with respect to f, then there exists x with p(x).

Русский

Если фильтр f не тривиален и P выполняется в пределе по f, тогда существует x, для которого p(x) истинно.

LaTeX

$$$ f \text{ nontrivial} \land (\forall^\! x \in f, p(x)) \rightarrow \exists x, p(x) $$$

Lean4

theorem «exists» {p : α → Prop} {f : Filter α} [NeBot f] (hp : ∀ᶠ x in f, p x) : ∃ x, p x :=
  hp.frequently.exists

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