Theorems · Definition

Set.Nonempty

{α : Type u} → Set α → Prop

The property s.Nonempty expresses the fact that the set s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Defined in

Mathlib.Data.Set.Defs

Cited by

2,627 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 8 definitions · uses no axioms