Mathlib Map

Theorems · Theorem · combinatorics

Finset.coe_nonempty

∀ {α : Type u_1} {s : Finset α}, (↑s).Nonempty ↔ s.Nonempty
Defined in
Mathlib.Data.Finset.Empty
Cited by
18 results in Mathlib
Foundations
Depth 55 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.

Finset.image₂_nonempty_iff · cited by 14Finset.image₂_nonempty_iffFinset.Nonempty.to_set · cited by 7Nonempty.to_setFinset.image_const · cited by 5Finset.image_constFinset.nonempty_Icc · cited by 3Finset.nonempty_IccFinset.univ_nonempty_iff · cited by 2Finset.univ_nonempty_iffSet.powersetCard.coe_nonempty_iff · cited by 2powersetCard.coe_nonempty…Finset.card_le_card_of_forall_subsingleton · cited by 2Finset.card_le_card_of_fo…Set.toFinset_nonempty · cited by 2Set.toFinset_nonemptySet.Finite.toFinset_nonempty · cited by 2Finite.toFinset_nonemptyFinset.coe_infsep · cited by 2Finset.coe_infsepDynamics.IsDynCoverOf.iterate_le_pow · cited by 2IsDynCoverOf.iterate_le_p…Finset.nonempty_Ico · cited by 1Finset.nonempty_IcoFinset.nonempty_Ioc · cited by 1Finset.nonempty_IocIsApproximateAddSubgroup.card_nsmul_le · cited by 1IsApproximateAddSubgroup.…Caratheodory.minCardFinsetOfMemConvexHull_nonempty · cited by 1Caratheodory.minCardFinse…Finset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeSet.Nonempty · cited by 2627Set.NonemptyFinset.Nonempty · cited by 1001Finset.NonemptyFinset.coe_nonemptyCITED BYCITES

Cites4

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

Cited by18

Results whose statement or proof uses this declaration.