Theorems · Definition · general topology
tsupport
{X : Type u_1} → {α : Type u_2} → [Zero α] → [TopologicalSpace X] → (X → α) → Set XThe topological support of a function is the closure of its support. i.e. the closure of the set of all elements where the function is nonzero.
- Defined in
- Mathlib.Topology.Algebra.Support
- Cited by
- 178 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 31 definitions · uses no axioms
- Assumes
- ZeroTopologicalSpace
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.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- closureproof · cited by 1,254
- Function.supportproof · cited by 610
Cited by194
Results whose statement or proof uses this declaration.
- HasCompactSupportproof · cited by 196
- Distribution.IsVanishingOnproof · cited by 27
- image_eq_zero_of_notMem_tsupportstatement and proof · cited by 24
- subset_tsupportstatement · cited by 21
- isClosed_tsupportstatement · cited by 17
- BumpCovering.IsSubordinateproof · cited by 15
- SmoothPartitionOfUnity.IsSubordinateproof · cited by 10
- PartitionOfUnity.IsSubordinateproof · cited by 10
- SmoothBumpCovering.IsSubordinateproof · cited by 7
- notMem_tsupport_iff_eventuallyEqstatement · cited by 7
- HasCompactSupport.isCompactstatement · cited by 5
- HasCompactSupport.tsupport_extend_zero_subsetstatement · cited by 5