eventually_exists_iff — Mathlib

English

If β is finite, then (∀ᶠ i in f, ∃ a ∈ β, P(a,i)) is equivalent to ∃ a ∈ β, ∀ᶠ i in f, P(a,i).

Русский

Если β конечен, то (∀ᶠ i in f, ∃ a ∈ β, P(a,i)) эквивалентно ∃ a ∈ β, ∀ᶠ i in f, P(a,i).

LaTeX

$$$\forall f\;\bigl( (\forall^{\infty} i \in f, \exists a\in \beta, P a i) \iff \exists a\in \beta, \forall^{\infty} i \in f, P a i \bigr)$$$

Lean4

theorem eventually_exists_iff [Finite β] {P : β → α → Prop} : (∀ᶠ i in f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ i in f, P a i := by
  simpa using eventually_exists_mem_iff (f := f) (P := P) Set.finite_univ

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