Filter.EventuallyConst.eventuallyEq_const
theorem Filter.EventuallyConst.eventuallyEq_const :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [inst : Nonempty β],
Filter.EventuallyConst f l → ∃ c, l.EventuallyEq f fun x => c
This theorem, termed as an alias of the forward direction of `Filter.eventuallyConst_iff_exists_eventuallyEq`, states that for any types `α` and `β`, a filter `l` on `α`, and a function `f` from `α` to `β`, given that type `β` is nonempty, if the function `f` is eventually constant along the filter `l` (as defined by `Filter.EventuallyConst`), then there exists a constant `c` such that the function `f` is eventually equivalent to the function that always returns `c` for all inputs (expressed as `l.EventuallyEq f fun x => c`). In simpler terms, if a function stabilizes to a constant value under a certain filter, we can find that constant.
More concisely: If a filter on a type `α` makes a function from `α` to a nonempty type `β` eventually constant, then there exists a constant value `c` such that the function is eventually equal to the constant function `c`.
|
Filter.EventuallyConst.comp
theorem Filter.EventuallyConst.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β},
Filter.EventuallyConst f l → ∀ (g : β → γ), Filter.EventuallyConst (g ∘ f) l
The theorem `Filter.EventuallyConst.comp` states that for any types `α`, `β`, and `γ`, and any filter `l` on `α` and functions `f` from `α` to `β` and `g` from `β` to `γ`, if the function `f` is eventually constant along the filter `l`, then the composition of `g` and `f` (denoted as `g ∘ f`) is also eventually constant along the filter `l`. Essentially, this theorem indicates that the property of being "eventually constant" is preserved under function composition.
More concisely: If a function `f : α → β` is eventually constant along a filter `l` on `α`, then the composition `g ∘ f` of `g : β → γ` with `f` is also eventually constant along `l`.
|
Filter.EventuallyConst.exists_tendsto
theorem Filter.EventuallyConst.exists_tendsto :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [inst : Nonempty β],
Filter.EventuallyConst f l → ∃ x, Filter.Tendsto f l (pure x)
The theorem `Filter.EventuallyConst.exists_tendsto` states that given any types `α` and `β`, a filter `l` on `α`, and a function `f` from `α` to `β`, if `β` is nonempty and the function `f` is eventually constant along the filter `l`, then there exists some value `x` such that `f` tends towards `x` along the filter `l`. In mathematical terms, if for some neighborhood of values in the codomain `β`, all function values fall into that neighborhood beyond a certain point in the domain `α`, then there exists a limit point `x` in `β` such that every neighborhood of `x` has a corresponding neighborhood on `α` whose image falls into the neighborhood of `x`.
More concisely: If a filter on a type `α` makes a function from `α` to a nonempty `β` eventually constant, then there exists a limit point in `β` that is the limit of the function along the filter.
|
Filter.EventuallyConst.comp₂
theorem Filter.EventuallyConst.comp₂ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {f : α → β} {g : α → γ},
Filter.EventuallyConst f l →
∀ (op : β → γ → δ), Filter.EventuallyConst g l → Filter.EventuallyConst (fun x => op (f x) (g x)) l
The theorem `Filter.EventuallyConst.comp₂` states that for any types `α`, `β`, `γ`, and `δ`, and any filter `l` on `α`, if a function `f` from `α` to `β` is eventually constant along `l`, and a function `g` from `α` to `γ` is also eventually constant along `l`, then for any binary operation `op` from `β` and `γ` to `δ`, the function which maps `x` in `α` to `op (f x) (g x)` in `δ` is also eventually constant along `l`. In other words, the composite function of two functions that are eventually constant along a filter is also eventually constant along that filter.
More concisely: If functions `f` and `g` are eventually constant along filter `l` on type `α`, then their composition `x ↦ op (f x) (g x)` is also eventually constant along filter `l`, where `op` is a binary operation from `β` and `γ` to `δ`.
|