Theorems · Definition · complex analysis
Function.locallyFinsuppWithin.toClosedBall
{E : Type u_1} →
[inst : NormedAddCommGroup E] →
(r : ℝ) → Function.locallyFinsupp E ℤ →+ Function.locallyFinsuppWithin (Metric.closedBall 0 |r|) ℤShorthand notation for the restriction of a function with locally finite support to the closed unit
ball of radius r.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- Set.univstatement · cited by 3,945
- AddMonoidHomstatement · cited by 3,230
- absstatement and proof · cited by 1,814
- Metric.closedBallstatement and proof · cited by 704
- Function.locallyFinsuppWithinstatement · cited by 127
- Function.locallyFinsuppstatement · cited by 43
- Function.locallyFinsuppWithin.restrictMonoidHomproof · cited by 2
Cited by11
Results whose statement or proof uses this declaration.
- Function.locallyFinsuppWithin.logCountingproof · cited by 36
- Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_constproof · cited by 4
- Function.locallyFinsuppWithin.toClosedBall_eval_withinstatement · cited by 3
- Function.locallyFinsuppWithin.logCounting_nonnegproof · cited by 3
- Function.locallyFinsuppWithin.logCounting_eval_zeroproof · cited by 2
- Function.locallyFinsuppWithin.logCounting_monoproof · cited by 2
- Function.locallyFinsuppWithin.toClosedBall_divisorstatement · cited by 1
- Function.locallyFinsuppWithin.toClosedBall_support_subset_closedBallstatement · cited by 1
- ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zeroproof · cited by 1
- Function.locallyFinsuppWithin.logCounting_evenproof · cited by 1