Functions that are eventually constant along a filter #
In this file we define a predicate
Filter.EventuallyConst f l saying that a function
f : α → β
is eventually equal to a constant along a filter
l. We also prove some basic properties of these
Implementation notes #
A naive definition of
Filter.EventuallyConst f l is
∃ y, ∀ᶠ x in l, f x = y.
However, this proposition is false for empty
Instead, we say that
Filter.map f l is supported on a subsingleton.
This allows us to drop
[Nonempty _] assumptions here and there.