Mathlib Map

Theorems · Theorem · order theory

Set.subset_singleton_iff_eq

∀ {α : Type u_1} {s : Set α} {x : α}, s ⊆ {x} ↔ s = ∅ ∨ s = {x}
Defined in
Mathlib.Data.Set.Insert
Cited by
10 results in Mathlib
Foundations
Depth 22 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.

Set.Nontrivial.not_subset_singleton · cited by 5Nontrivial.not_subset_sin…Set.Nonempty.subset_singleton_iff · cited by 5Nonempty.subset_singleton…Matroid.IsBase.exchange_isBase_of_indep · cited by 3IsBase.exchange_isBase_of…Set.ssubset_singleton_iff · cited by 2Set.ssubset_singleton_iffsSup_eq_bot' · cited by 1sSup_eq_bot'Profinite.NobelingProof.GoodProducts.P0 · cited by 1GoodProducts.P0gauge_of_subset_zero · cited by 1gauge_of_subset_zeroSet.subset_one_iff_eq · cited by 0Set.subset_one_iff_eqSet.subset_zero_iff_eq · cited by 0Set.subset_zero_iff_eqsInf_eq_top' · cited by 0sInf_eq_top'Set · cited by 53352SetSet.subset_singleton_iff_eqCITED BYCITES

Cites1

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

  • Setstatement and proof · cited by 53,352

Cited by10

Results whose statement or proof uses this declaration.