Theorems · Definition · general topology
mulTSupport
{X : Type u_1} → {α : Type u_2} → [One α] → [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 not equal to 1.
- Defined in
- Mathlib.Topology.Algebra.Support
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- OneTopologicalSpace
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.mulSupportproof · cited by 240
Cited by42
Results whose statement or proof uses this declaration.
- HasCompactMulSupportproof · cited by 43
- subset_mulTSupportstatement · cited by 6
- isClosed_mulTSupportstatement · cited by 5
- HasCompactMulSupport.mulTSupport_extend_one_subsetstatement · cited by 4
- mulTSupport_binop_subsetstatement · cited by 3
- notMem_mulTSupport_iff_eventuallyEqstatement · cited by 3
- continuous_of_mulTSupportstatement and proof · cited by 2
- image_eq_one_of_notMem_mulTSupportstatement and proof · cited by 2
- mulTSupport_fun_invstatement · cited by 1
- mulTSupport_onestatement · cited by 1
- HasCompactMulSupport.comp_isClosedEmbeddingproof · cited by 1
- HasCompactMulSupport.isCompactstatement · cited by 1