# Empty and nonempty finite sets #

This file defines the empty finite set ∅ and a predicate for nonempty `Finset`s.

## Main declarations #

- `Finset.Nonempty`: A finset is nonempty if it has elements. This is equivalent to saying `s ≠ ∅`.
- `Finset.empty`: Denoted by `∅`. The finset associated to any type consisting of no elements.

## Tags #

finite sets, finset

### Nonempty #

source
def Finset.Nonempty {α : Type u_1} (s : Finset α) :
Prop

The property `s.Nonempty` expresses the fact that the finset `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.

Equations

- s.Nonempty = ∃ (x : α), x ∈ s

Instances For

source
theorem Finset.nonempty_def {α : Type u_1} {s : Finset α} :
s.Nonempty ↔ ∃ (x : α), x ∈ s
source
instance Finset.decidableNonempty {α : Type u_1} {s : Finset α} :
Decidable s.Nonempty
Equations

- Finset.decidableNonempty = decidable_of_iff (∃ a ∈ s, true = true) ⋯

source
@[simp]
theorem Finset.coe_nonempty {α : Type u_1} {s : Finset α} :
(↑s).Nonempty ↔ s.Nonempty
source
theorem Finset.nonempty_coe_sort {α : Type u_1} {s : Finset α} :
Nonempty ↥s ↔ s.Nonempty
source
theorem Finset.Nonempty.to_set {α : Type u_1} {s : Finset α} :
s.Nonempty → (↑s).Nonempty

Alias of the reverse direction of `Finset.coe_nonempty`.

source
theorem Finset.Nonempty.coe_sort {α : Type u_1} {s : Finset α} :
s.Nonempty → Nonempty ↥s

Alias of the reverse direction of `Finset.nonempty_coe_sort`.

source
theorem Finset.Nonempty.exists_mem {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
∃ (x : α), x ∈ s
source
theorem Finset.Nonempty.mono {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) (hs : s.Nonempty) :
t.Nonempty
source
theorem Finset.Nonempty.forall_const {α : Type u_1} {s : Finset α} (h : s.Nonempty) {p : Prop} :
(∀ x ∈ s, p) ↔ p
source
theorem Finset.Nonempty.to_subtype {α : Type u_1} {s : Finset α} :
s.Nonempty → Nonempty ↥s
source
theorem Finset.Nonempty.to_type {α : Type u_1} {s : Finset α} :
s.Nonempty → Nonempty α

### empty #

source
def Finset.empty {α : Type u_1} :
Finset α

The empty finset

Equations

- Finset.empty = { val := 0, nodup := ⋯ }

Instances For

source
instance Finset.instEmptyCollection {α : Type u_1} :
EmptyCollection (Finset α)
Equations

- Finset.instEmptyCollection = { emptyCollection := Finset.empty }

source
instance Finset.inhabitedFinset {α : Type u_1} :
Inhabited (Finset α)
Equations

- Finset.inhabitedFinset = { default := ∅ }

source
@[simp]
theorem Finset.empty_val {α : Type u_1} :
∅.val = 0
source
@[simp]
theorem Finset.notMem_empty {α : Type u_1} (a : α) :
a ∉ ∅
source
@[deprecated Finset.notMem_empty (since := "2025-05-23")]
theorem Finset.not_mem_empty {α : Type u_1} (a : α) :
a ∉ ∅

Alias of `Finset.notMem_empty`.

source
@[simp]
theorem Finset.not_nonempty_empty {α : Type u_1} :
¬∅.Nonempty
source
@[simp]
theorem Finset.mk_zero {α : Type u_1} :
{ val := 0, nodup := ⋯ } = ∅
source
theorem Finset.ne_empty_of_mem {α : Type u_1} {a : α} {s : Finset α} (h : a ∈ s) :
s ≠ ∅
source
theorem Finset.Nonempty.ne_empty {α : Type u_1} {s : Finset α} (h : s.Nonempty) :
s ≠ ∅
source
@[simp]
theorem Finset.empty_subset {α : Type u_1} (s : Finset α) :
∅ ⊆ s
source
theorem Finset.eq_empty_of_forall_notMem {α : Type u_1} {s : Finset α} (H : ∀ (x : α), x ∉ s) :
s = ∅
source
@[deprecated Finset.eq_empty_of_forall_notMem (since := "2025-05-23")]
theorem Finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : Finset α} (H : ∀ (x : α), x ∉ s) :
s = ∅

Alias of `Finset.eq_empty_of_forall_notMem`.

source
theorem Finset.eq_empty_iff_forall_notMem {α : Type u_1} {s : Finset α} :
s = ∅ ↔ ∀ (x : α), x ∉ s
source
@[deprecated Finset.eq_empty_iff_forall_notMem (since := "2025-05-23")]
theorem Finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : Finset α} :
s = ∅ ↔ ∀ (x : α), x ∉ s

Alias of `Finset.eq_empty_iff_forall_notMem`.

source
@[simp]
theorem Finset.val_eq_zero {α : Type u_1} {s : Finset α} :
s.val = 0 ↔ s = ∅
source
@[simp]
theorem Finset.subset_empty {α : Type u_1} {s : Finset α} :
s ⊆ ∅ ↔ s = ∅
source
@[simp]
theorem Finset.not_ssubset_empty {α : Type u_1} (s : Finset α) :
¬s ⊂ ∅
source
theorem Finset.nonempty_of_ne_empty {α : Type u_1} {s : Finset α} (h : s ≠ ∅) :
s.Nonempty
source
theorem Finset.nonempty_iff_ne_empty {α : Type u_1} {s : Finset α} :
s.Nonempty ↔ s ≠ ∅
source
@[simp]
theorem Finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : Finset α} :
¬s.Nonempty ↔ s = ∅
source
theorem Finset.eq_empty_or_nonempty {α : Type u_1} (s : Finset α) :
s = ∅ ∨ s.Nonempty
source
@[simp]
theorem Finset.coe_empty {α : Type u_1} :
↑∅ = ∅
source
@[simp]
theorem Finset.coe_eq_empty {α : Type u_1} {s : Finset α} :
↑s = ∅ ↔ s = ∅
source
@[simp]
theorem Finset.isEmpty_coe_sort {α : Type u_1} {s : Finset α} :
IsEmpty ↥s ↔ s = ∅
source
instance Finset.instIsEmpty {α : Type u_1} :
IsEmpty ↥∅
source
theorem Finset.eq_empty_of_isEmpty {α : Type u_1} [IsEmpty α] (s : Finset α) :
s = ∅

A `Finset` for an empty type is empty.

source
instance Finset.instOrderBot {α : Type u_1} :
OrderBot (Finset α)
Equations

- Finset.instOrderBot = { bot := ∅, bot_le := ⋯ }

source
@[simp]
theorem Finset.bot_eq_empty {α : Type u_1} :
⊥ = ∅
source
@[simp]
theorem Finset.empty_ssubset {α : Type u_1} {s : Finset α} :
∅ ⊂ s ↔ s.Nonempty
source
theorem Finset.Nonempty.empty_ssubset {α : Type u_1} {s : Finset α} :
s.Nonempty → ∅ ⊂ s

Alias of the reverse direction of `Finset.empty_ssubset`.

source
theorem Finset.exists_mem_empty_iff {α : Type u_1} (p : α → Prop) :
(∃ x ∈ ∅, p x) ↔ False
source
theorem Finset.forall_mem_empty_iff {α : Type u_1} (p : α → Prop) :
(∀ x ∈ ∅, p x) ↔ True
source
def Mathlib.Meta.proveFinsetNonempty {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) :
Lean.MetaM (Option Q(«$s».Nonempty))

Attempt to prove that a finset is nonempty using the `finsetNonempty` aesop rule-set.

You can add lemmas to the rule-set by tagging them with either:

- `aesop safe apply (rule_sets := [finsetNonempty])` if they are always a good idea to follow or
- `aesop unsafe apply (rule_sets := [finsetNonempty])` if they risk directing the search to a blind alley.

TODO: should some of the lemmas be `aesop safe simp` instead?

Equations

- One or more equations did not get rendered due to their size.

Instances For