eventually_exists_mem_iff — Mathlib

English

If is is finite, then (∀ᶠ i in f, ∃ a ∈ is, P(a,i)) holds if and only if ∃ a ∈ is such that ∀ᶠ i in f, P(a,i).

Русский

Пусть is конечен. Тогда (∀ᶠ i in f, ∃ a ∈ is, P(a,i)) эквивалентно ∃ a ∈ is, ∀ᶠ i in f, P(a,i).

LaTeX

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

Lean4

theorem eventually_exists_mem_iff {is : Set β} {P : β → α → Prop} (his : is.Finite) :
    (∀ᶠ i in f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ i in f, P a i :=
  by
  simp only [Filter.Eventually, Ultrafilter.mem_coe]
  convert f.finite_biUnion_mem_iff his (s := P) with i
  aesop

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