Empty and nonempty finite sets

This file defines the empty finite set ∅ and a predicate for nonempty Finsets.

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

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

theorem Finset.nonempty_def {α : Type u_1} {s : Finset α} : s.Nonempty ↔ ∃ (x : α), x ∈ s

instance Finset.decidableNonempty {α : Type u_1} {s : Finset α} : Decidable s.Nonempty

Equations

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

@[simp]

theorem Finset.coe_nonempty {α : Type u_1} {s : Finset α} : (↑s).Nonempty ↔ s.Nonempty

theorem Finset.nonempty_coe_sort {α : Type u_1} {s : Finset α} : Nonempty ↥s ↔ s.Nonempty

theorem Finset.Nonempty.to_set {α : Type u_1} {s : Finset α} : s.Nonempty → (↑s).Nonempty

Alias of the reverse direction of Finset.coe_nonempty.

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

Alias of the reverse direction of Finset.nonempty_coe_sort.

theorem Finset.Nonempty.exists_mem {α : Type u_1} {s : Finset α} (h : s.Nonempty) : ∃ (x : α), x ∈ s

theorem Finset.Nonempty.mono {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) (hs : s.Nonempty) : t.Nonempty

theorem Finset.Nonempty.forall_const {α : Type u_1} {s : Finset α} (h : s.Nonempty) {p : Prop} : (∀ x ∈ s, p) ↔ p

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

theorem Finset.Nonempty.to_type {α : Type u_1} {s : Finset α} : s.Nonempty → Nonempty α

empty

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

The empty finset

Equations

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

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

Equations

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

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

Equations

• Finset.inhabitedFinset = { default := ∅ }

@[simp]

theorem Finset.empty_val {α : Type u_1} : ∅.val = 0

@[simp]

theorem Finset.notMem_empty {α : Type u_1} (a : α) : a ∉ ∅

@[deprecated Finset.notMem_empty (since := "2025-05-23")]

theorem Finset.not_mem_empty {α : Type u_1} (a : α) : a ∉ ∅

Alias of Finset.notMem_empty.

@[simp]

theorem Finset.not_nonempty_empty {α : Type u_1} : ¬∅.Nonempty

@[simp]

theorem Finset.mk_zero {α : Type u_1} : { val := 0, nodup := ⋯ } = ∅

theorem Finset.ne_empty_of_mem {α : Type u_1} {a : α} {s : Finset α} (h : a ∈ s) : s ≠ ∅

theorem Finset.Nonempty.ne_empty {α : Type u_1} {s : Finset α} (h : s.Nonempty) : s ≠ ∅

@[simp]

theorem Finset.empty_subset {α : Type u_1} (s : Finset α) : ∅ ⊆ s

theorem Finset.eq_empty_of_forall_notMem {α : Type u_1} {s : Finset α} (H : ∀ (x : α), x ∉ s) : s = ∅

@[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.

theorem Finset.eq_empty_iff_forall_notMem {α : Type u_1} {s : Finset α} : s = ∅ ↔ ∀ (x : α), x ∉ s

@[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.

@[simp]

theorem Finset.val_eq_zero {α : Type u_1} {s : Finset α} : s.val = 0 ↔ s = ∅

@[simp]

theorem Finset.subset_empty {α : Type u_1} {s : Finset α} : s ⊆ ∅ ↔ s = ∅

@[simp]

theorem Finset.not_ssubset_empty {α : Type u_1} (s : Finset α) : ¬s ⊂ ∅

theorem Finset.nonempty_of_ne_empty {α : Type u_1} {s : Finset α} (h : s ≠ ∅) : s.Nonempty

theorem Finset.nonempty_iff_ne_empty {α : Type u_1} {s : Finset α} : s.Nonempty ↔ s ≠ ∅

@[simp]

theorem Finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : Finset α} : ¬s.Nonempty ↔ s = ∅

theorem Finset.eq_empty_or_nonempty {α : Type u_1} (s : Finset α) : s = ∅ ∨ s.Nonempty

@[simp]

theorem Finset.coe_empty {α : Type u_1} : ↑∅ = ∅

@[simp]

theorem Finset.coe_eq_empty {α : Type u_1} {s : Finset α} : ↑s = ∅ ↔ s = ∅

@[simp]

theorem Finset.isEmpty_coe_sort {α : Type u_1} {s : Finset α} : IsEmpty ↥s ↔ s = ∅

instance Finset.instIsEmpty {α : Type u_1} : IsEmpty ↥∅

theorem Finset.eq_empty_of_isEmpty {α : Type u_1} [IsEmpty α] (s : Finset α) : s = ∅

A Finset for an empty type is empty.

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

Equations

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

@[simp]

theorem Finset.bot_eq_empty {α : Type u_1} : ⊥ = ∅

@[simp]

theorem Finset.empty_ssubset {α : Type u_1} {s : Finset α} : ∅ ⊂ s ↔ s.Nonempty

theorem Finset.Nonempty.empty_ssubset {α : Type u_1} {s : Finset α} : s.Nonempty → ∅ ⊂ s

Alias of the reverse direction of Finset.empty_ssubset.

theorem Finset.exists_mem_empty_iff {α : Type u_1} (p : α → Prop) : (∃ x ∈ ∅, p x) ↔ False

theorem Finset.forall_mem_empty_iff {α : Type u_1} (p : α → Prop) : (∀ x ∈ ∅, p x) ↔ True

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.