inter_eventuallyEq_left — Mathlib

English

Let l be a filter on α and s,t subsets of α. Then (s ∩ t) is eventually equal to s along l if and only if for l-almost every x, x ∈ s implies x ∈ t.

Русский

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

LaTeX

$$$(s \\cap t : Set α) =ᶠ[l] s \\iff ∀ᶠ x in l, x ∈ s \\to x ∈ t$$$

Lean4

theorem inter_eventuallyEq_left {s t : Set α} {l : Filter α} : (s ∩ t : Set α) =ᶠ[l] s ↔ ∀ᶠ x in l, x ∈ s → x ∈ t := by
  simp only [eventuallyEq_set, mem_inter_iff, and_iff_left_iff_imp]

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