Structures · Topology
SummationFilter.HasSupport
Typeclass asserting that the sets in L.filter are eventually contained in L.support. This
is a sufficient condition for L-summation to behave well on finitely-supported functions: every
finitely-supported f is L-summable with the sum ∑ᶠ x ∈ L.support, f x (and similarly for
products).
- Shape
- One type argument · adds eventually_le_support
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- summable_of_hasFiniteSupport
- SummationFilter.HasSupport.eventually_le_support
- Summable.of_finite
- summable_of_ne_finset_zero
- multipliable_of_hasFiniteMulSupport
- hasProd_fintype_support
- hasProd_prod_support_of_ne_finset_one
- hasSum_fintype_support
- SummationFilter.eventually_mem_or_not_mem
- hasSum_sum_support_of_ne_finset_zero
- Multipliable.of_finite
- multipliable_of_ne_finset_one
- Finset.hasProd_support
- Finset.hasSum_support
- SummationFilter.instHasSupportMap
- multipliable_of_finite_mulSupport
- summable_of_finite_support
- Function.Injective.hasSum_comap_iff_of_hasSupport
- SummationFilter.instHasSupportComap
- Function.Injective.hasProd_comap_iff_of_hasSupport
Ancestors0
No ancestors.