eventuallyEq_set — Mathlib

English

Filtration equality of sets along a filter is equivalent to pointwise membership agreement along the filter.

Русский

Эквивалентность по фильтру множеств эквивалентна согласованности по членству на каждом элементе фильтра.

LaTeX

$$$s =^{{l}} t \\iff \\forall^{{\\text{freq}}}_{x\\in l} (x\\in s \\iff x\\in t)$$$

Lean4

theorem eventuallyEq_set {s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ s ↔ x ∈ t :=
  eventually_congr <| Eventually.of_forall fun _ ↦ eq_iff_iff

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