mem_limsup_iff_frequently_mem — Mathlib

English

For s(i) and 𝓕, a ∈ limsup s 𝓕 iff a occurs frequently in s(i) along 𝓕.

Русский

Для s(i) и 𝓕, a принадлежит limsup s 𝓕 тогда и только тогда, когда a встречается часто в s(i) вдоль 𝓕.

LaTeX

$$(a ∈ limsup s 𝓕) ⇔ (∃ᶠ i in 𝓕, a ∈ s i)$$

Lean4

theorem mem_limsup_iff_frequently_mem : (a ∈ limsup s 𝓕) ↔ (∃ᶠ i in 𝓕, a ∈ s i) := by
  simp only [Filter.Frequently, iff_not_comm, ← mem_compl_iff, limsup_compl, comp_apply, mem_liminf_iff_eventually_mem]

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