Filter.const_boundedAtFilter
theorem Filter.const_boundedAtFilter :
∀ {α : Type u_2} {β : Type u_3} [inst : Norm β] (l : Filter α) (c : β), l.BoundedAtFilter (Function.const α c) := by
sorry
This theorem states that for any type `α` and any normed field `β`, for any filter `l` on `α` and any constant `c` from `β`, the constant function (which always returns `c`, regardless of the input) is bounded at the filter `l`. In other words, the rate of growth of a constant function is always bounded when evaluated at any filter.
More concisely: For any type `α`, normed field `β`, filter `l` on `α`, and constant `c` from `β`, the constant function from `α` to `β` that maps every element to `c` is bounded at `l`.
|
Filter.zero_zeroAtFilter
theorem Filter.zero_zeroAtFilter :
∀ {α : Type u_2} {β : Type u_3} [inst : Zero β] [inst_1 : TopologicalSpace β] (l : Filter α), l.ZeroAtFilter 0 := by
sorry
This theorem states that for any filter `l` on a type `α` in the context of a topological space on type `β` that has a zero, the constant zero function is `ZeroAtFilter` along `l`. In other words, the constant function that always maps to zero tends towards zero along any filter `l`.
More concisely: For any filter `l` on type `α` in a topological space with a zero, the constant zero function is the limit of any sequence in `α` along `l`.
|