set_eventuallyEq_iff_inf_principal

English

For sets s,t and filter l, s =ᶠ[l] t if and only if l ⊓ 𝓟 s = l ⊓ 𝓟 t.

Русский

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

LaTeX

$$$$ s =^l t \\iff l \\wedge 𝓟 s = l \\wedge 𝓟 t. $$$$

Lean4

theorem set_eventuallyEq_iff_inf_principal {s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t := by
  simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]

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