eventuallyEq_empty — Mathlib

English

Let l be a filter on α and s a subset of α. Then s is eventually empty along l if and only if for l-almost every x, x is not in s.

Русский

Пусть l — фильтр на α, и s — подмножество α. Тогда s равно пустому по лям фильтра тогда и только тогда, когда для почти всех x относительно l выполняется x ∉ s.

LaTeX

$$$ s =ᶠ[l] (\\emptyset : Set α) \\iff ∀ᶠ x in l, x ∉ s $$$

Lean4

theorem eventuallyEq_empty {s : Set α} {l : Filter α} : s =ᶠ[l] (∅ : Set α) ↔ ∀ᶠ x in l, x ∉ s :=
  eventuallyEq_set.trans <| by simp

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