Theorems · Theorem · general algebraic systems
Function.support_subset_iff
∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set ι},
Function.support f ⊆ s ↔ ∀ (x : ι), f x ≠ 0 → x ∈ s- Defined in
- Mathlib.Algebra.Notation.Support
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- Function.supportstatement · cited by 610
Cited by7
Results whose statement or proof uses this declaration.
- tsum_subtype_eq_of_support_subsetproof · cited by 7
- finsum_add_distribproof · cited by 4
- finsum_eq_finsetSum_of_support_subsetproof · cited by 3
- Function.locallyFinsuppWithin.eq_zero_codiscreteWithinproof · cited by 2
- Multiset.support_fun_nsmul_count_subsetproof · cited by 2
- finsum_applyproof · cited by 0
- Equiv.tsum_eq_tsum_of_supportproof · cited by 0