Mathlib Map

Theorems · Theorem · combinatorics

Finset.coe_eq_singleton

∀ {α : Type u_1} {s : Finset α} {a : α}, ↑s = {a} ↔ s = {a}
Defined in
Mathlib.Data.Finset.Insert
Cited by
9 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.Icc_self · cited by 12Finset.Icc_selfFinset.eq_singleton_or_nontrivial · cited by 6Finset.eq_singleton_or_no…Finset.Icc_eq_singleton_iff · cited by 2Finset.Icc_eq_singleton_i…Finset.local_lubell_yamamoto_meshalkin_inequality_mul · cited by 2Finset.local_lubell_yamam…IsLocalRing.primesOverFinset_eq · cited by 1IsLocalRing.primesOverFin…SimpleGraph.incMatrix_mul_transpose_apply_of_adj · cited by 1SimpleGraph.incMatrix_mul…Finset.coe_eq_one · cited by 0Finset.coe_eq_oneFinset.coe_eq_zero · cited by 0Finset.coe_eq_zeroFinset.isAddUnit_coe · cited by 0Finset.isAddUnit_coeSet · cited by 53352SetFinset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeFinset.coe_eq_singletonCITED 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 by9

Results whose statement or proof uses this declaration.