set_eventuallyLE_iff_mem_inf_principal

English

For sets s,t, and filter l, s ≤ᶠ[l] t is equivalent to t belonging to the infimum of l and the principal filter of s.

Русский

Для множеств s,t и фильтра l выполнение s ≤ᶠ[l] t эквивалентно тому, что t принадлежит частному пределу l и принципиальному фильтру s.

LaTeX

$$$$ s \\leq^{\\!l} t \\quad\\iff\\quad t \\in l \\;\\sqcap\\; 𝓟 s. $$$$

Lean4

theorem set_eventuallyLE_iff_mem_inf_principal {s t : Set α} {l : Filter α} : s ≤ᶠ[l] t ↔ t ∈ l ⊓ 𝓟 s :=
  eventually_inf_principal.symm

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