Mathlib Map

Theorems · Theorem · logic and foundations

Subsingleton.mem_iff_nonempty

∀ {α : Type u_2} [Subsingleton α] {s : Set α} {x : α}, x ∈ s ↔ s.Nonempty
Defined in
Mathlib.Data.Set.Basic
Cited by
3 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Subsingleton
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.surjOn_of_subsingleton' · cited by 2Set.surjOn_of_subsingleto…Set.mapsTo_of_subsingleton' · cited by 2Set.mapsTo_of_subsingleto…Subsingleton.convexIndependent · cited by 0Subsingleton.convexIndepe…Set · cited by 53352SetSet.Nonempty · cited by 2627Set.NonemptySubsingleton.mem_iff_nonemptyCITED BYCITES

Cites2

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
  • Set.Nonemptystatement and proof · cited by 2,627

Cited by3

Results whose statement or proof uses this declaration.