Theorems · Definition · general topology
Function.locallyFinsuppWithin.single
{X : Type u_1} →
[inst : TopologicalSpace X] →
{Y : Type u_2} → [DecidableEq X] → [inst_2 : Zero Y] → X → Y → Function.locallyFinsupp X YIs analogy to Finsupp.single, this definition presents the indicator function
of a single point as a function with locally finite support.
- Defined in
- Mathlib.Topology.LocallyFinsupp
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Function.supportproof · cited by 610
- Pi.singleproof · cited by 518
- Function.locallyFinsuppstatement · cited by 43
Cited by18
Results whose statement or proof uses this declaration.
- Function.locallyFinsuppWithin.single_applystatement · cited by 8
- Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_conststatement and proof · cited by 4
- Function.locallyFinsuppWithin.single_posstatement · cited by 3
- Function.locallyFinsuppWithin.coe_singlestatement · cited by 2
- Function.locallyFinsuppWithin.sum_apply_smul_single_eq_self_on_univstatement and proof · cited by 1
- Function.locallyFinsuppWithin.zero_iff_logCounting_boundedproof · cited by 1
- Function.locallyFinsuppWithin.logCounting_isBigO_log_of_finite_supportproof · cited by 1
- Function.locallyFinsuppWithin.logCounting_single_isBigO_logstatement and proof · cited by 1
- Function.locallyFinsuppWithin.logCounting_strictMonostatement and proof · cited by 1
- Function.locallyFinsuppWithin.one_isLittleO_logCounting_singlestatement · cited by 1
- Function.locallyFinsuppWithin.exists_single_le_posstatement · cited by 1
- Function.locallyFinsuppWithin.finite_support_of_logCounting_isBigO_logproof · cited by 1