set_eventuallyLE_iff_inf_principal_le

English

For sets s,t and filter l, s ≤ᶠ[l] t is equivalent to l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t.

Русский

Для множеств s,t и фильтра l, s ≤ᶠ[l] t эквивалентно l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t.

LaTeX

$$$$ s \\leq^{\\!l} t \\iff l \\wedge 𝓟 s \\le l \\wedge 𝓟 t. $$$$

Lean4

theorem set_eventuallyLE_iff_inf_principal_le {s t : Set α} {l : Filter α} : s ≤ᶠ[l] t ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t :=
  set_eventuallyLE_iff_mem_inf_principal.trans <| by simp only [le_inf_iff, inf_le_left, true_and, le_principal_iff]

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