exists_mem — Mathlib

English

If f and g are frequently equal, there exists a set in the filter where f and g agree pointwise.

Русский

Если f и g часто совпадают, существует множество S в фильтре, на котором f и g совпадают точечно.

LaTeX

$$$\\exists S\\in l, \\forall x\\in S,\n f(x)=g(x)$$$

Lean4

theorem exists_mem {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) : ∃ s ∈ l, EqOn f g s :=
  Eventually.exists_mem h

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