mem_liminf_iff_eventually_mem — Mathlib

English

For a family of sets s(i), filter 𝓕, and an element a, a ∈ liminf s 𝓕 if and only if a ∈ s(i) eventually for i in 𝓕.

Русский

Для семейства множеств s(i) и фильтра 𝓕 верно: a ∈ liminf s 𝓕 тогда и только тогда, когда a принадлежит s(i) для большинства i в 𝓕.

LaTeX

$$(a ∈ liminf s 𝓕) ⇔ (∀ᶠ i in 𝓕, a ∈ s i)$$

Lean4

theorem mem_liminf_iff_eventually_mem : (a ∈ liminf s 𝓕) ↔ (∀ᶠ i in 𝓕, a ∈ s i) := by
  simpa only [liminf_eq_iSup_iInf, iSup_eq_iUnion, iInf_eq_iInter, mem_iUnion, mem_iInter] using
    ⟨fun ⟨S, hS, hS'⟩ ↦ mem_of_superset hS (by tauto), fun h ↦ ⟨{i | a ∈ s i}, h, by tauto⟩⟩

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