Theorems · Theorem · general topology
notMem_tsupport_iff_eventuallyEq
∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {x : α},
x ∉ tsupport f ↔ f =ᶠ[nhds x] 0- Defined in
- Mathlib.Topology.Algebra.Support
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- nhdsstatement and proof · cited by 5,554
- Filter.EventuallyEqstatement and proof · cited by 1,912
- Set.EqOnproof · cited by 603
- tsupportstatement · cited by 178
- Set.not_nonempty_iff_eq_emptyproof · cited by 56
- Set.disjoint_iff_inter_eq_emptyproof · cited by 49
- mem_closure_iff_nhdsproof · cited by 20
- Filter.eventuallyEq_iff_exists_memproof · cited by 19
- Function.disjoint_support_iffproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- contMDiff_of_tsupportproof · cited by 4
- continuous_of_tsupportproof · cited by 3
- HasStrictDerivAt.of_notMem_tsupportproof · cited by 1
- HasStrictFDerivAt.of_notMem_tsupportproof · cited by 1
- fderiv_of_notMem_tsupportproof · cited by 1
- deriv_of_notMem_tsupportproof · cited by 1
- contMDiffWithinAt_of_notMemproof · cited by 1