Theorems · Theorem · logic and foundations
Set.mem_empty_iff_false
∀ {α : Type u} (x : α), x ∈ ∅ ↔ False- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 32 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 by32
Results whose statement or proof uses this declaration.
- finsum_zeroproof · cited by 18
- Function.support_eq_empty_iffproof · cited by 7
- nhds_bot_orderproof · cited by 4
- iInf_emptysetproof · cited by 3
- infClosed_emptyproof · cited by 2
- ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPointproof · cited by 2
- Set.Finite.iInf_biSup_of_monotoneproof · cited by 2
- Set.Finite.iUnionproof · cited by 2
- finsum_mem_emptyproof · cited by 2
- IsClopen.continuous_indicatorproof · cited by 2
- Seminorm.ball_eq_emptysetproof · cited by 2
- csInf_eq_csInf_of_forall_exists_leproof · cited by 1