Theorems · Theorem · combinatorics
Finset.val_eq_zero
∀ {α : Type u_1} {s : Finset α}, s.val = 0 ↔ s = ∅- Defined in
- Mathlib.Data.Finset.Empty
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Quot.sound
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.
- Finsetstatement and proof · cited by 13,712
- Multisetstatement · cited by 2,627
- Finset.valstatement · cited by 438
- Finset.val_injproof · cited by 9
Cited by12
Results whose statement or proof uses this declaration.
- Finset.card_eq_zeroproof · cited by 34
- Finset.sum_lt_sum_of_nonemptyproof · cited by 10
- Finset.nonempty_of_ne_emptyproof · cited by 9
- Finset.subset_emptyproof · cited by 4
- Finset.le_sum_nonempty_of_subadditive_on_predproof · cited by 3
- Finset.sum_induction_nonemptyproof · cited by 2
- Finset.toList_eq_nilproof · cited by 2
- Multiset.Ico_eq_zero_iffproof · cited by 1
- Finset.sym2_eq_emptyproof · cited by 1
- Multiset.Ioc_eq_zero_iffproof · cited by 1
- Multiset.Icc_eq_zero_iffproof · cited by 1
- Multiset.Ioo_eq_zero_iffproof · cited by 0