Mathlib Map

Theorems · Theorem · combinatorics

Finset.coe_eq_empty

∀ {α : Type u_1} {s : Finset α}, ↑s = ∅ ↔ s = ∅
Defined in
Mathlib.Data.Finset.Empty
Cited by
8 results in Mathlib
Foundations
Depth 58 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.Ioi_eq_empty · cited by 4Finset.Ioi_eq_emptySet.Intersecting.is_max_iff_card_eq · cited by 2Intersecting.is_max_iff_c…Finset.Ico_eq_empty_iff · cited by 2Finset.Ico_eq_empty_iffFinset.Ioc_eq_empty_iff · cited by 2Finset.Ioc_eq_empty_iffFinset.Icc_eq_empty_iff · cited by 2Finset.Icc_eq_empty_iffdisjointed_of_isMin · cited by 1disjointed_of_isMinaddDissociated_empty · cited by 1addDissociated_emptyFinset.Ioo_eq_empty_iff · cited by 1Finset.Ioo_eq_empty_iffSet · cited by 53352SetFinset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeFinset.coe_eq_emptyCITED 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 by8

Results whose statement or proof uses this declaration.