Mathlib Map

Theorems · Theorem · logic and foundations

Set.not_nonempty_empty

∀ {α : Type u}, ¬∅.Nonempty
Defined in
Mathlib.Data.Set.Basic
Cited by
5 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Filter.forall_mem_nonempty_iff_neBot · cited by 4Filter.forall_mem_nonempt…Cardinal.sInf_empty · cited by 2Cardinal.sInf_emptyCountableInfClosed.empty · cited by 1CountableInfClosed.emptyOrdinal.sInf_empty · cited by 0Ordinal.sInf_emptynot_bddBelow_univ · cited by 0not_bddBelow_univSet · cited by 53352SetSet.Nonempty · cited by 2627Set.NonemptySet.not_nonempty_emptyCITED BYCITES

Cites2

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

  • Setstatement · cited by 53,352
  • Set.Nonemptystatement and proof · cited by 2,627

Cited by5

Results whose statement or proof uses this declaration.