Theorems · Theorem · logic and foundations
Set.notMem_empty
∀ {α : Type u} (x : α), x ∉ ∅- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 4 from the axioms · 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 · cited by 53,352
Cited by35
Results whose statement or proof uses this declaration.
- Matroid.isNonloop_of_looplessproof · cited by 6
- Nat.notMem_of_lt_sInfproof · cited by 4
- Matroid.isLoop_tfaeproof · cited by 3
- TopologicalSpace.IsTopologicalBasis.sdiff_emptyproof · cited by 3
- Matroid.closure_exchangeproof · cited by 3
- CompactExhaustion.find_shiftrproof · cited by 2
- IsCyclotomicExtension.iff_union_singleton_oneproof · cited by 2
- MvPolynomial.transcendental_polynomial_aeval_Xproof · cited by 2
- MeasureTheory.mem_generateSetAlgebra_elimproof · cited by 1
- SimpleGraph.incMatrix_apply_mul_incMatrix_apply_of_not_adjproof · cited by 1
- Setoid.empty_notMem_classesproof · cited by 1
- cbiSup_emptyproof · cited by 1