Theorems · Definition · general topology

Filter.EventuallyEq

{α : Type u_1} → {β : Type u_2} → Filter α → (α → β) → (α → β) → Prop

Two functions f and g are eventually equal along a filter l if the set of x such that f x = g x belongs to l.

Defined in

Mathlib.Order.Filter.Defs

Cited by

1,912 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 13 definitions · uses no axioms