Theorems · Theorem · general topology
subset_tsupport
∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
Function.support f ⊆ tsupport f- Defined in
- Mathlib.Topology.Algebra.Support
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroTopologicalSpace
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.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Function.supportstatement · cited by 610
- subset_closureproof · cited by 309
- tsupportstatement · cited by 178
Cited by21
Results whose statement or proof uses this declaration.
- image_eq_zero_of_notMem_tsupportproof · cited by 24
- Continuous.integrable_of_hasCompactSupportproof · cited by 18
- HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroupproof · cited by 4
- HasCompactSupport.isCompact_preimageproof · cited by 4
- HasCompactSupport.isCompact_rangeproof · cited by 4
- HasCompactSupport.eq_zero_or_locallyCompactSpace_of_groupproof · cited by 3
- Continuous.stronglyMeasurable_of_hasCompactSupportproof · cited by 3
- IsOpen.exists_contDiff_support_eqproof · cited by 2
- MeasureTheory.integral_integral_swap_of_hasCompactSupportproof · cited by 2
- IsOpen.exists_contMDiff_support_eqproof · cited by 1
- MeasureTheory.continuous_integral_apply_inv_mulproof · cited by 1
- MeasureTheory.continuous_integral_apply_neg_addproof · cited by 1