exists — Mathlib

English

If p holds frequently with respect to f, then there exists an x with p(x).

Русский

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

LaTeX

$$$ (\exists^\! x \in f, p(x)) \rightarrow \exists x, p(x) $$$

Lean4

theorem «exists» {p : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x) : ∃ x, p x :=
  by
  by_contra H
  replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)
  exact hp H

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