Theorems · Definition · general topology
Function.locallyFinsuppWithin.support
{X : Type u_1} →
[inst : TopologicalSpace X] →
{U : Set X} → {Y : Type u_2} → [inst_1 : Zero Y] → Function.locallyFinsuppWithin U Y → Set XThis allows writing D.support instead of Function.support D
- Defined in
- Mathlib.Topology.LocallyFinsupp
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpaceZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Function.supportproof · cited by 610
- Function.locallyFinsuppWithinstatement and proof · cited by 127
Cited by29
Results whose statement or proof uses this declaration.
- Function.locallyFinsuppWithin.supportWithinDomainstatement · cited by 12
- Function.locallyFinsuppWithin.finiteSupportstatement · cited by 9
- Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomainstatement · cited by 6
- MeromorphicOn.extract_zeros_polesstatement and proof · cited by 4
- MeromorphicOn.extract_zeros_poles_logproof · cited by 3
- MeromorphicOn.circleAverage_log_normproof · cited by 3
- MeromorphicOn.divisor_ball_support_finitestatement · cited by 3
- Function.locallyFinsuppWithin.logCounting_monoproof · cited by 2
- divisor_sphere_support_finitestatement · cited by 2
- Function.locallyFinsuppWithin.eq_zero_codiscreteWithinproof · cited by 2
- Complex.ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAtproof · cited by 1
- Function.locallyFinsuppWithin.logCounting_isBigO_log_of_finite_supportstatement and proof · cited by 1