inter_eventuallyEq_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_eventuallyEq_right {s t : Set α} {l : Filter α} : (s ∩ t : Set α) =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ t → x ∈ s := by
  rw [inter_comm, inter_eventuallyEq_left]

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