Theorems · Theorem · logic and foundations

Set.nonempty_of_ncard_ne_zero

∀ {α : Type u_1} {s : Set α}, s.ncard ≠ 0 → s.Nonempty

Defined in: Mathlib.Data.Set.Card
Cited by: 5 results in Mathlib
Foundations: Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Setstatement and proof · cited by 53,352
Set.Nonemptystatement · cited by 2,627
Set.ncardstatement and proof · cited by 344
Set.nonempty_iff_ne_emptyproof · cited by 96
Set.ncard_emptyproof · cited by 14

Cited by5

Results whose statement or proof uses this declaration.

Setoid.IsPartition.ncard_eq_finsumproof · cited by 2
SimpleGraph.ncard_oddComponents_monoproof · cited by 1
Set.fiber_ncard_ne_zero_iff_mem_imageproof · cited by 0
SimpleGraph.Walk.IsCycle.adj_toSubgraph_iff_of_isCyclesproof · cited by 0
SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSuppproof · cited by 0