eventuallyEq_inf_principal_iff — Mathlib

English

Let F be a filter on α and s a subset of α. Then f =ᶠ[F ⊓ 𝓟 s] g iff for ∀ᶠ x in F, x ∈ s → f x = g x.

Русский

Пусть F — фильтр на α и s ⊆ α. Тогда f =ᶠ[F ⊓ 𝓟 s] g тогда и только тогда, когда для почти всех x в F, если x ∈ s, то f x = g x.

LaTeX

$$$ f =ᶠ[F \\inf 𝓟 s] g \\iff ∀ᶠ x in F, x ∈ s \\to f x = g x $$$

Lean4

theorem eventuallyEq_inf_principal_iff {F : Filter α} {s : Set α} {f g : α → β} :
    f =ᶠ[F ⊓ 𝓟 s] g ↔ ∀ᶠ x in F, x ∈ s → f x = g x :=
  eventually_inf_principal

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