Mathlib Map

Theorems · Theorem · combinatorics

Finset.notMem_empty

∀ {α : Type u_1} (a : α), a ∉ ∅
Defined in
Mathlib.Data.Finset.Empty
Cited by
40 results in Mathlib
Foundations
Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finset.disjoint_left · cited by 50Finset.disjoint_leftFinset.sum_eq_zero_iff_of_nonneg · cited by 19Finset.sum_eq_zero_iff_of…Finset.mem_sym_iff · cited by 9Finset.mem_sym_iffFinset.product_empty · cited by 7Finset.product_emptyMeasureTheory.Measure.haar.addIndex_pos · cited by 5haar.addIndex_posFinset.not_nonempty_empty · cited by 5Finset.not_nonempty_emptyhasSum_sum · cited by 4hasSum_sumSet.mem_finsetSum · cited by 4Set.mem_finsetSumFinset.inf_eq_top_iff · cited by 3Finset.inf_eq_top_iffFinset.mem_sigmaLift · cited by 3Finset.mem_sigmaLiftSet.mem_finsetProd · cited by 3Set.mem_finsetProdFinset.ne_empty_of_mem · cited by 3Finset.ne_empty_of_memFinset.prod_eq_one_iff_of_one_le' · cited by 3Finset.prod_eq_one_iff_of…Finset.mem_sumLift₂ · cited by 2Finset.mem_sumLift₂Finset.indicator_biUnion · cited by 2Finset.indicator_biUnionFinset · cited by 13712FinsetFinset.notMem_emptyCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Finsetstatement · cited by 13,712

Cited by40

Results whose statement or proof uses this declaration.