eventuallyEq_of_mem

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Set.EqOn.eventuallyEq_of_mem

← MathLib Explorer

English

If f and g are equal on s and s ∈ l, then f =ᶠ[l] g.

Русский

Если f и g равны на s и s принадлежит фильтру l, то f =ᶠ[l] g.

LaTeX

$$$$ \\text{EqOn}(f,g,s) \\land s \\in l \\Rightarrow f =^l g. $$$$

Lean4

theorem eventuallyEq_of_mem {α β} {s : Set α} {l : Filter α} {f g : α → β} (h : EqOn f g s) (hl : s ∈ l) : f =ᶠ[l] g :=
  h.eventuallyEq.filter_mono <| Filter.le_principal_iff.2 hl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru