Mathlib Map

Theorems · Theorem · combinatorics

Finset.mem_coe

∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ ↑s ↔ a ∈ s
Defined in
Mathlib.Data.Finset.Defs
Cited by
91 results in Mathlib
Foundations
Depth 54 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.

MeasureTheory.SimpleFunc.induction · cited by 14SimpleFunc.inductionMatrix.det_fromBlocks_zero₂₁ · cited by 10Matrix.det_fromBlocks_zer…Polynomial.mem_rootSet' · cited by 8Polynomial.mem_rootSet'isOpen_pi_iff · cited by 6isOpen_pi_iffFinset.map_subtype_subset · cited by 5Finset.map_subtype_subsetIsDedekindDomain.mem_primesOverFinset_iff · cited by 4IsDedekindDomain.mem_prim…affineIndependent_iff_indicator_eq_of_affineCombination_eq · cited by 4affineIndependent_iff_ind…AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan · cited by 4AffineIndependent.eq_zero…Fintype.card_lt_of_injective_of_notMem · cited by 4Fintype.card_lt_of_inject…Finset.convexHull_eq · cited by 4Finset.convexHull_eqAddMonoid.exponent_ne_zero_iff_range_addOrderOf_finite · cited by 3AddMonoid.exponent_ne_zer…Finset.ruzsa_triangle_inequality_div_div_div · cited by 3Finset.ruzsa_triangle_ine…finprod_prod_comm · cited by 3finprod_prod_commFinset.ruzsa_triangle_inequality_sub_sub_sub · cited by 3Finset.ruzsa_triangle_ine…Nat.sum_div_divisors · cited by 3Nat.sum_div_divisorsSet · cited by 53352SetFinset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeFinset.mem_coeCITED BYCITES

Cites3

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

  • Setstatement · cited by 53,352
  • Finsetstatement and proof · cited by 13,712
  • SetLike.coestatement · cited by 8,199

Cited by91

Results whose statement or proof uses this declaration.