Zero and Bounded at filter #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Given a filter l
we define the notion of a function being zero_at_filter
as well as being
bounded_at_filter
. Alongside this we construct the submodule
, add_submonoid
of functions
that are zero_at_filter
. Similarly, we construct the submodule
and subalgebra
of functions
that are bounded_at_filter
.
If l
is a filter on α
, then a function f : α → β
is zero_at_filter l
if it tends to zero along l
.
Equations
- l.zero_at_filter f = filter.tendsto f l (nhds 0)
zero_at_filter_submodule l
is the submodule of f : α → β
which
tend to zero along l
.
Equations
- l.zero_at_filter_submodule = {carrier := l.zero_at_filter, add_mem' := _, zero_mem' := _, smul_mem' := _}
zero_at_filter_add_submonoid l
is the additive submonoid of f : α → β
which tend to zero along l
.
Equations
- l.zero_at_filter_add_submonoid = {carrier := l.zero_at_filter, add_mem' := _, zero_mem' := _}
The submodule of functions that are bounded along a filter l
.
Equations
- l.bounded_filter_submodule = {carrier := l.bounded_at_filter, add_mem' := _, zero_mem' := _, smul_mem' := _}
The subalgebra of functions that are bounded along a filter l
.