eventuallyEq_iff_all_subsets — Mathlib

English

Let f,g be functions α → β. Then f ≈ g along l iff for every subset s of α, f and g are eventually equal on s (i.e., f and g agree on s for all x in l).

Русский

Пусть f,g : α → β. Тогда f =ᶠ[l] g эквивалентно тому, что для каждого подмножества s ⊆ α выполняется f и g совпадают на s в смысле l.

LaTeX

$$$ f =ᶠ[l] g \\iff ∀ s : Set α, ∀ᶠ x in l, x ∈ s \\to f x = g x $$$

Lean4

theorem eventuallyEq_iff_all_subsets {f g : α → β} {l : Filter α} :
    f =ᶠ[l] g ↔ ∀ s : Set α, ∀ᶠ x in l, x ∈ s → f x = g x :=
  eventually_iff_all_subsets

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