Theorems · Definition
Set.Elem
{α : Type u} → Set α → Type uGiven the set s, Elem s is the Type of element of s.
It is currently an abbreviation so that instance coming from Subtype are available.
If you're interested in making it a def, as it probably should be,
you'll then need to create additional instances (and possibly prove lemmas about them).
See e.g. Mathlib/Data/Set/Order.lean.
- Defined in
- Mathlib.Data.Set.CoeSort
- Cited by
- 7,166 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 8 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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 by8,584
Results whose statement or proof uses this declaration.
- Set.Finiteproof · cited by 1,814
- Set.Countableproof · cited by 545
- Set.domRestrictstatement and proof · cited by 383
- Set.encardproof · cited by 327
- Set.Finite.subsetproof · cited by 285
- Set.toFinsetstatement and proof · cited by 217
- LinearIndepOnproof · cited by 211
- Set.toFinitestatement and proof · cited by 174
- Set.inclusionstatement and proof · cited by 145
- Module.Free.ChooseBasisIndexproof · cited by 133
- SimpleGraph.edgeFinsetstatement and proof · cited by 116
- SimpleGraph.degreestatement and proof · cited by 112
Showing the 200 most cited of 8,584.