Mathlib Map

Theorems · Theorem

not_isEmpty_iff

∀ {α : Sort u_1}, ¬IsEmpty α ↔ Nonempty α
Defined in
Mathlib.Logic.IsEmpty.Basic
Cited by
19 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isEmpty_or_nonempty · cited by 269isEmpty_or_nonemptyCardinal.mk_ne_zero_iff · cited by 11Cardinal.mk_ne_zero_iffnot_isEmpty_of_nonempty · cited by 8not_isEmpty_of_nonemptyRelEmbedding.not_wellFounded · cited by 5RelEmbedding.not_wellFoun…Filter.NeBot.nonempty · cited by 4NeBot.nonemptyWithTop.iInf_coe_lt_top · cited by 2WithTop.iInf_coe_lt_topCategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty · cited by 2PreGaloisCategory.not_ini…Subgroup.exists_finiteIndex_of_leftCoset_cover_aux · cited by 2Subgroup.exists_finiteInd…AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux · cited by 2AddSubgroup.exists_finite…AffineBasis.nonempty · cited by 2AffineBasis.nonemptyOrder.krullDim_ne_bot_iff · cited by 1Order.krullDim_ne_bot_iffENat.iInf_natCast_ne_top · cited by 1ENat.iInf_natCast_ne_topnonempty_fun · cited by 1nonempty_funSimpleGraph.chromaticNumber_eq_one_iff · cited by 1SimpleGraph.chromaticNumb…RelEmbedding.not_acc · cited by 1RelEmbedding.not_accIsEmpty · cited by 759IsEmptynot_iff_comm · cited by 32not_iff_commnot_nonempty_iff · cited by 20not_nonempty_iffnot_isEmpty_iffCITED BYCITES

Cites3

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

Cited by19

Results whose statement or proof uses this declaration.