doc-next-gen

Mathlib.Data.Finset.Insert

Module docstring

{"# Constructing finite sets by adding one element

This file contains the definitions of {a} : Finset α, insert a s : Finset α and Finset.cons, all ways to construct a Finset by adding one element.

Main declarations

  • Finset.induction_on: Induction on finsets. To prove a proposition about an arbitrary Finset α, it suffices to prove it for the empty finset, and to show that if it holds for some Finset α, then it holds for the finset obtained by inserting a new element.
  • Finset.instSingletonFinset: Denoted by {a}; the finset consisting of one element.
  • insert and Finset.cons: For any a : α, insert s a returns s ∪ {a}. cons s a h returns the same except that it requires a hypothesis stating that a is not already in s. This does not require decidable equality on the type α.

Tags

finite sets, finset

","### Subset and strict subset relations ","### singleton ","### cons ","### insert "}

Finset.instSingleton instance
: Singleton α (Finset α)
Full source 
/-- `{a} : Finset a` is the set `{a}` containing `a` and nothing else.

This differs from `insert a ∅` in that it does not require a `DecidableEq` instance for `α`.
-/
instance : Singleton α (Finset α) :=
  ⟨fun a => ⟨{a}, nodup_singleton a⟩⟩
Singleton Finite Set Construction
Informal description
For any type $\alpha$, there is a singleton operation that constructs a finite set containing exactly one element $a \in \alpha$. This differs from inserting $a$ into the empty set in that it does not require decidable equality on $\alpha$.
Finset.singleton_val theorem
(a : α) : ({ a } : Finset α).1 = { a }
Full source 
@[simp]
theorem singleton_val (a : α) : ({a} : Finset α).1 = {a} :=
  rfl
Underlying Multiset of Singleton Finset
Informal description
For any element $a$ of type $\alpha$, the underlying multiset of the singleton finite set $\{a\}$ is equal to the singleton multiset $\{a\}$.
Finset.mem_singleton_self theorem
(a : α) : a ∈ ({ a } : Finset α)
Full source 
theorem mem_singleton_self (a : α) : a ∈ ({a} : Finset α) :=
  mem_singleton.mpr rfl
Self-Membership in Singleton Finite Set: $a \in \{a\}$
Informal description
For any element $a$ of type $\alpha$, the element $a$ belongs to the singleton finite set $\{a\}$.
Finset.val_eq_singleton_iff theorem
{a : α} {s : Finset α} : s.val = { a } ↔ s = { a }
Full source 
@[simp]
theorem val_eq_singleton_iff {a : α} {s : Finset α} : s.val = {a} ↔ s = {a} := by
  rw [← val_inj]
  rfl
Equivalence of Singleton Multiset and Singleton Finite Set
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the underlying multiset of $s$ is equal to the singleton multiset $\{a\}$ if and only if $s$ is equal to the singleton finite set $\{a\}$.
Finset.singleton_injective theorem
: Injective (singleton : α → Finset α)
Full source 
theorem singleton_injective : Injective (singleton : α → Finset α) := fun _a _b h =>
  mem_singleton.1 (h ▸ mem_singleton_self _)
Injectivity of the Singleton Construction for Finite Sets
Informal description
The singleton construction function $\{ \cdot \} : \alpha \to \text{Finset } \alpha$ is injective. That is, for any elements $a, b \in \alpha$, if $\{a\} = \{b\}$ as finite sets, then $a = b$.
Finset.singleton_inj theorem
: ({ a } : Finset α) = { b } ↔ a = b
Full source 
@[simp]
theorem singleton_inj : ({a} : Finset α) = {b} ↔ a = b :=
  singleton_injective.eq_iff
Equality of Singleton Finite Sets: $\{a\} = \{b\} \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the singleton finite sets $\{a\}$ and $\{b\}$ are equal if and only if $a = b$.
Finset.singleton_nonempty theorem
(a : α) : ({ a } : Finset α).Nonempty
Full source 
@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
theorem singleton_nonempty (a : α) : ({a} : Finset α).Nonempty :=
  ⟨a, mem_singleton_self a⟩
Nonempty Singleton Finite Set
Informal description
For any element $a$ of type $\alpha$, the singleton finite set $\{a\}$ is nonempty.
Finset.singleton_ne_empty theorem
(a : α) : ({ a } : Finset α) ≠ ∅
Full source 
@[simp]
theorem singleton_ne_empty (a : α) : ({a} : Finset α) ≠ ∅ :=
  (singleton_nonempty a).ne_empty
Non-emptiness of Singleton Finite Sets: $\{a\} \neq \emptyset$
Informal description
For any element $a$ of type $\alpha$, the singleton finite set $\{a\}$ is not equal to the empty set $\emptyset$.
Finset.coe_singleton theorem
(a : α) : (({ a } : Finset α) : Set α) = { a }
Full source 
@[simp, norm_cast]
theorem coe_singleton (a : α) : (({a} : Finset α) : Set α) = {a} := by
  ext
  simp
Equality of Singleton Finite Set and Singleton Set: $\{a\} = \{a\}$
Informal description
For any element $a$ of type $\alpha$, the underlying set of the singleton finite set $\{a\}$ is equal to the singleton set $\{a\}$ in the type of sets over $\alpha$.
Finset.coe_eq_singleton theorem
{s : Finset α} {a : α} : (s : Set α) = { a } ↔ s = { a }
Full source 
@[simp, norm_cast]
theorem coe_eq_singleton {s : Finset α} {a : α} : (s : Set α) = {a} ↔ s = {a} := by
  rw [← coe_singleton, coe_inj]
Equivalence of Finite Set and Singleton Set: $\{a\}$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the underlying set of $s$ is equal to the singleton set $\{a\}$ if and only if $s$ is the singleton finite set $\{a\}$.
Finset.coe_subset_singleton theorem
: (s : Set α) ⊆ { a } ↔ s ⊆ { a }
Full source 
@[norm_cast]
lemma coe_subset_singleton : (s : Set α) ⊆ {a}(s : Set α) ⊆ {a} ↔ s ⊆ {a} := by rw [← coe_subset, coe_singleton]
Subset Correspondence Between Set and Singleton Finite Set: $s \subseteq \{a\} \leftrightarrow s \subseteq \{a\}$
Informal description
For any set $s$ and element $a$ of type $\alpha$, the set $s$ is a subset of the singleton set $\{a\}$ if and only if the finite set corresponding to $s$ is a subset of the singleton finite set $\{a\}$.
Finset.singleton_subset_coe theorem
: { a } ⊆ (s : Set α) ↔ { a } ⊆ s
Full source 
@[norm_cast]
lemma singleton_subset_coe : {a}{a} ⊆ (s : Set α){a} ⊆ (s : Set α) ↔ {a} ⊆ s := by rw [← coe_subset, coe_singleton]
Singleton Subset Correspondence: $\{a\} \subseteq s \leftrightarrow \{a\} \subseteq \text{toSet}(s)$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the singleton set $\{a\}$ is a subset of the underlying set of $s$ if and only if the singleton finite set $\{a\}$ is a subset of $s$.
Finset.nonempty_iff_eq_singleton_default theorem
[Unique α] {s : Finset α} : s.Nonempty ↔ s = { default }
Full source 
theorem nonempty_iff_eq_singleton_default [Unique α] {s : Finset α} :
    s.Nonempty ↔ s = {default} := by
  simp [eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton]
Nonempty Finite Subset Equals Singleton of Default in Unique Type
Informal description
For a type $\alpha$ with a unique element (denoted as `default`), a finite subset $s$ of $\alpha$ is nonempty if and only if $s$ is equal to the singleton set $\{\text{default}\}$.
Finset.singleton_iff_unique_mem theorem
(s : Finset α) : (∃ a, s = { a }) ↔ ∃! a, a ∈ s
Full source 
theorem singleton_iff_unique_mem (s : Finset α) : (∃ a, s = {a}) ↔ ∃! a, a ∈ s := by
  simp only [eq_singleton_iff_unique_mem, ExistsUnique]
Characterization of Singleton Finite Sets via Unique Membership
Informal description
For any finite set $s$ of type $\alpha$, $s$ is a singleton set (i.e., there exists an element $a \in \alpha$ such that $s = \{a\}$) if and only if there exists a unique element $a \in s$.
Finset.singleton_subset_set_iff theorem
{s : Set α} {a : α} : ↑({ a } : Finset α) ⊆ s ↔ a ∈ s
Full source 
theorem singleton_subset_set_iff {s : Set α} {a : α} : ↑({a} : Finset α) ⊆ s↑({a} : Finset α) ⊆ s ↔ a ∈ s := by
  rw [coe_singleton, Set.singleton_subset_iff]
Singleton Finite Set Subset Criterion: $\{a\} \subseteq s \leftrightarrow a \in s$
Informal description
For any set $s$ over a type $\alpha$ and any element $a \in \alpha$, the singleton finite set $\{a\}$ is a subset of $s$ (when viewed as a set) if and only if $a$ is an element of $s$.
Finset.singleton_subset_iff theorem
{s : Finset α} {a : α} : { a } ⊆ s ↔ a ∈ s
Full source 
@[simp]
theorem singleton_subset_iff {s : Finset α} {a : α} : {a}{a} ⊆ s{a} ⊆ s ↔ a ∈ s :=
  singleton_subset_set_iff
Singleton Subset Criterion: $\{a\} \subseteq s \leftrightarrow a \in s$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the singleton finite set $\{a\}$ is a subset of $s$ if and only if $a$ is an element of $s$.
Finset.subset_singleton_iff theorem
{s : Finset α} {a : α} : s ⊆ { a } ↔ s = ∅ ∨ s = { a }
Full source 
@[simp]
theorem subset_singleton_iff {s : Finset α} {a : α} : s ⊆ {a}s ⊆ {a} ↔ s = ∅ ∨ s = {a} := by
  rw [← coe_subset, coe_singleton, Set.subset_singleton_iff_eq, coe_eq_empty, coe_eq_singleton]
Characterization of Finite Subsets of a Singleton: $s \subseteq \{a\} \leftrightarrow s = \emptyset \lor s = \{a\}$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, $s$ is a subset of the singleton set $\{a\}$ if and only if $s$ is either the empty set or the singleton set $\{a\}$ itself. In other words, $s \subseteq \{a\} \leftrightarrow s = \emptyset \lor s = \{a\}$.
Finset.singleton_subset_singleton theorem
: ({ a } : Finset α) ⊆ { b } ↔ a = b
Full source 
theorem singleton_subset_singleton : ({a} : Finset α) ⊆ {b}({a} : Finset α) ⊆ {b} ↔ a = b := by simp
Subset Relation between Singleton Finite Sets: $\{a\} \subseteq \{b\} \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the singleton finite set $\{a\}$ is a subset of the singleton finite set $\{b\}$ if and only if $a = b$.
Finset.Nonempty.subset_singleton_iff theorem
{s : Finset α} {a : α} (h : s.Nonempty) : s ⊆ { a } ↔ s = { a }
Full source 
protected theorem Nonempty.subset_singleton_iff {s : Finset α} {a : α} (h : s.Nonempty) :
    s ⊆ {a}s ⊆ {a} ↔ s = {a} :=
  subset_singleton_iff.trans <| or_iff_right h.ne_empty
Nonempty Subset of Singleton Characterization: $s \subseteq \{a\} \leftrightarrow s = \{a\}$ for nonempty $s$
Informal description
For any nonempty finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the set $s$ is a subset of the singleton set $\{a\}$ if and only if $s$ is equal to $\{a\}$.
Finset.subset_singleton_iff' theorem
{s : Finset α} {a : α} : s ⊆ { a } ↔ ∀ b ∈ s, b = a
Full source 
theorem subset_singleton_iff' {s : Finset α} {a : α} : s ⊆ {a}s ⊆ {a} ↔ ∀ b ∈ s, b = a :=
  forall₂_congr fun _ _ => mem_singleton
Characterization of Subset of Singleton: $s \subseteq \{a\} \leftrightarrow \forall b \in s, b = a$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the set $s$ is a subset of the singleton set $\{a\}$ if and only if every element $b \in s$ satisfies $b = a$.
Finset.ssubset_singleton_iff theorem
{s : Finset α} {a : α} : s ⊂ { a } ↔ s = ∅
Full source 
@[simp]
theorem ssubset_singleton_iff {s : Finset α} {a : α} : s ⊂ {a}s ⊂ {a} ↔ s = ∅ := by
  rw [← coe_ssubset, coe_singleton, Set.ssubset_singleton_iff, coe_eq_empty]
Characterization of Strict Subset of Singleton: $s \subset \{a\} \leftrightarrow s = \emptyset$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the strict subset relation $s \subset \{a\}$ holds if and only if $s$ is the empty set.
Finset.Nontrivial abbrev
(s : Finset α) : Prop
Full source 
/-- A finset is nontrivial if it has at least two elements. -/
protected abbrev Nontrivial (s : Finset α) : Prop := (s : Set α).Nontrivial
Nontrivial Finite Set
Informal description
A finite set $s$ of type $\alpha$ is called *nontrivial* if there exist two distinct elements $x$ and $y$ in $s$, i.e., there exist $x \in s$ and $y \in s$ such that $x \neq y$.
Finset.Nontrivial.nonempty theorem
(hs : s.Nontrivial) : s.Nonempty
Full source 
nonrec lemma Nontrivial.nonempty (hs : s.Nontrivial) : s.Nonempty := hs.nonempty
Nontrivial finite sets are nonempty
Informal description
For any finite set $s$ of type $\alpha$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is nonempty.
Finset.not_nontrivial_empty theorem
: ¬(∅ : Finset α).Nontrivial
Full source 
@[simp]
theorem not_nontrivial_empty : ¬ (∅ : Finset α).Nontrivial := by simp [Finset.Nontrivial]
Empty Finite Set is Not Nontrivial
Informal description
The empty finite set $\emptyset$ (of type `Finset α`) is not nontrivial, i.e., it does not contain two distinct elements.
Finset.not_nontrivial_singleton theorem
: ¬({ a } : Finset α).Nontrivial
Full source 
@[simp]
theorem not_nontrivial_singleton : ¬ ({a} : Finset α).Nontrivial := by simp [Finset.Nontrivial]
Singleton Finite Sets Are Not Nontrivial
Informal description
For any element $a$ of type $\alpha$, the singleton finite set $\{a\}$ is not nontrivial (i.e., it does not contain two distinct elements).
Finset.Nontrivial.ne_singleton theorem
(hs : s.Nontrivial) : s ≠ { a }
Full source 
theorem Nontrivial.ne_singleton (hs : s.Nontrivial) : s ≠ {a} := by
  rintro rfl; exact not_nontrivial_singleton hs
Nontrivial Finite Set is Not a Singleton
Informal description
For any finite set $s$ of type $\alpha$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is not equal to the singleton set $\{a\}$ for any $a \in \alpha$.
Finset.Nontrivial.exists_ne theorem
(hs : s.Nontrivial) (a : α) : ∃ b ∈ s, b ≠ a
Full source 
nonrec lemma Nontrivial.exists_ne (hs : s.Nontrivial) (a : α) : ∃ b ∈ s, b ≠ a := hs.exists_ne _
Existence of Distinct Element in Nontrivial Finite Set
Informal description
For any nontrivial finite set $s$ of type $\alpha$ and any element $a \in \alpha$, there exists an element $b \in s$ such that $b \neq a$.
Finset.nontrivial_iff_ne_singleton theorem
(ha : a ∈ s) : s.Nontrivial ↔ s ≠ { a }
Full source 
theorem nontrivial_iff_ne_singleton (ha : a ∈ s) : s.Nontrivial ↔ s ≠ {a} :=
  ⟨Nontrivial.ne_singleton, (eq_singleton_or_nontrivial ha).resolve_left⟩
Nontrivial Finite Set Characterization: $s$ Nontrivial $\iff$ $s \neq \{a\}$ for $a \in s$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in s$, the set $s$ is nontrivial (contains at least two distinct elements) if and only if $s$ is not equal to the singleton set $\{a\}$.
Finset.Nonempty.exists_eq_singleton_or_nontrivial theorem
: s.Nonempty → (∃ a, s = { a }) ∨ s.Nontrivial
Full source 
theorem Nonempty.exists_eq_singleton_or_nontrivial : s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial :=
  fun ⟨a, ha⟩ => (eq_singleton_or_nontrivial ha).imp_left <| Exists.intro a
Classification of Nonempty Finite Sets: Singleton or Nontrivial
Informal description
For any nonempty finite set $s$, there exists an element $a \in s$ such that $s$ is equal to the singleton set $\{a\}$, or $s$ is nontrivial (i.e., contains at least two distinct elements).
Finset.nontrivial_coe theorem
: (s : Set α).Nontrivial ↔ s.Nontrivial
Full source 
@[simp, norm_cast] lemma nontrivial_coe : (s : Set α).Nontrivial ↔ s.Nontrivial := .rfl
Equivalence of Nontriviality for Finite Sets and Their Set Counterparts
Informal description
A finite set $s$ of type $\alpha$ is nontrivial (contains at least two distinct elements) if and only if its corresponding set $\{a \mid a \in s\}$ is nontrivial.
Finset.Nontrivial.not_subset_singleton theorem
(hs : s.Nontrivial) : ¬s ⊆ { a }
Full source 
lemma Nontrivial.not_subset_singleton (hs : s.Nontrivial) : ¬s ⊆ {a} :=
  mod_cast hs.coe.not_subset_singleton
Nontrivial Finite Sets Cannot Be Subsets of Singletons
Informal description
For any finite set $s$ of type $\alpha$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is not a subset of the singleton set $\{a\}$ for any element $a \in \alpha$.
Finset.instNontrivial instance
[Nonempty α] : Nontrivial (Finset α)
Full source 
instance instNontrivial [Nonempty α] : Nontrivial (Finset α) :=
  ‹Nonempty α›.elim fun a => ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩
Nontriviality of Finite Subsets of Nonempty Types
Informal description
For any nonempty type $\alpha$, the type of finite subsets of $\alpha$ is nontrivial (contains at least two distinct elements).
Finset.instUniqueOfIsEmpty instance
[IsEmpty α] : Unique (Finset α)
Full source 
instance [IsEmpty α] : Unique (Finset α) where
  default := ∅
  uniq _ := eq_empty_of_forall_not_mem isEmptyElim
Uniqueness of Finite Subsets of an Empty Type
Informal description
For any type $\alpha$ that is empty (has no elements), the type of finite subsets of $\alpha$ is unique (has exactly one element, the empty set).
Finset.instUniqueSubtypeMemSingleton instance
(i : α) : Unique ({ i } : Finset α)
Full source 
instance (i : α) : Unique ({i} : Finset α) where
  default := ⟨i, mem_singleton_self i⟩
  uniq j := Subtype.ext <| mem_singleton.mp j.2
Uniqueness of Singleton Finite Sets
Informal description
For any element $i$ of type $\alpha$, the finite subset $\{i\}$ has a unique structure, meaning there is exactly one way to construct it as a finite set.
Finset.default_singleton theorem
(i : α) : ((default : ({ i } : Finset α)) : α) = i
Full source 
@[simp]
lemma default_singleton (i : α) : ((default : ({i} : Finset α)) : α) = i := rfl
Default Element of Singleton Finite Set is Its Element
Informal description
For any element $i$ of type $\alpha$, the default element of the singleton finite set $\{i\}$ is equal to $i$ when coerced back to $\alpha$.
Finset.Nontrivial.instDecidablePred instance
[DecidableEq α] : DecidablePred (Finset.Nontrivial (α := α))
Full source 
instance Nontrivial.instDecidablePred [DecidableEq α] :
    DecidablePred (Finset.Nontrivial (α := α)) :=
  inferInstanceAs (DecidablePred fun s ↦ ∃ a ∈ s, ∃ b ∈ s, a ≠ b)
Decidability of Nontriviality for Finite Sets
Informal description
For any type $\alpha$ with decidable equality, the predicate "nontrivial" on finite subsets of $\alpha$ is decidable. That is, given a finite set $s \subseteq \alpha$, we can algorithmically determine whether $s$ contains at least two distinct elements.
Finset.cons definition
(a : α) (s : Finset α) (h : a ∉ s) : Finset α
Full source 
/-- `cons a s h` is the set `{a} ∪ s` containing `a` and the elements of `s`. It is the same as
`insert a s` when it is defined, but unlike `insert a s` it does not require `DecidableEq α`,
and the union is guaranteed to be disjoint. -/
def cons (a : α) (s : Finset α) (h : a ∉ s) : Finset α :=
  ⟨a ::ₘ s.1, nodup_cons.2 ⟨h, s.2⟩⟩
Disjoint union of a singleton and a finite set
Informal description
Given an element $a$ of type $\alpha$, a finite set $s$ of $\alpha$, and a proof $h$ that $a$ is not in $s$, the operation $\text{cons}(a, s, h)$ returns the finite set $\{a\} \cup s$. This operation does not require decidable equality on $\alpha$ and guarantees that the union is disjoint.
Finset.mem_cons theorem
{h} : b ∈ s.cons a h ↔ b = a ∨ b ∈ s
Full source 
@[simp]
theorem mem_cons {h} : b ∈ s.cons a hb ∈ s.cons a h ↔ b = a ∨ b ∈ s :=
  Multiset.mem_cons
Membership in Finite Set After Cons Operation: $b \in \text{cons}(a, s, h) \leftrightarrow b = a \lor b \in s$
Informal description
For any element $b$ of type $\alpha$, finite set $s$ of $\alpha$, and element $a$ not in $s$ (with proof $h$), we have $b \in \text{cons}(a, s, h)$ if and only if either $b = a$ or $b \in s$.
Finset.mem_cons_of_mem theorem
{a b : α} {s : Finset α} {hb : b ∉ s} (ha : a ∈ s) : a ∈ cons b s hb
Full source 
theorem mem_cons_of_mem {a b : α} {s : Finset α} {hb : b ∉ s} (ha : a ∈ s) : a ∈ cons b s hb :=
  Multiset.mem_cons_of_mem ha
Membership Preservation in Finite Set Construction: $a \in s \to a \in \text{cons}(b, s, hb)$
Informal description
For any elements $a, b$ of type $\alpha$ and any finite set $s$ of $\alpha$, if $a \in s$ and $b \notin s$, then $a \in \text{cons}(b, s, hb)$, where $\text{cons}(b, s, hb)$ denotes the finite set $\{b\} \cup s$.
Finset.mem_cons_self theorem
(a : α) (s : Finset α) {h} : a ∈ cons a s h
Full source 
theorem mem_cons_self (a : α) (s : Finset α) {h} : a ∈ cons a s h :=
  Multiset.mem_cons_self _ _
Self-Membership in Finite Set Construction: $a \in \text{cons}(a, s, h)$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of $\alpha$, if $a \notin s$ (with proof $h$), then $a$ is an element of the finite set $\text{cons}(a, s, h)$.
Finset.cons_val theorem
(h : a ∉ s) : (cons a s h).1 = a ::ₘ s.1
Full source 
@[simp]
theorem cons_val (h : a ∉ s) : (cons a s h).1 = a ::ₘ s.1 :=
  rfl
Underlying Multiset of Finite Set Construction: $\text{cons}(a, s, h).1 = a ::ₘ s.1$
Informal description
For any element $a$ of type $\alpha$ and finite set $s$ of $\alpha$, if $a \notin s$ (with proof $h$), then the underlying multiset of $\text{cons}(a, s, h)$ is equal to $a$ prepended to the underlying multiset of $s$.
Finset.mem_of_mem_cons_of_ne theorem
{s : Finset α} {a : α} {has} {i : α} (hi : i ∈ cons a s has) (hia : i ≠ a) : i ∈ s
Full source 
theorem mem_of_mem_cons_of_ne {s : Finset α} {a : α} {has} {i : α}
    (hi : i ∈ cons a s has) (hia : i ≠ a) : i ∈ s :=
  (mem_cons.1 hi).resolve_left hia
Membership in Cons Set Implies Membership in Original Set for Non-Added Elements
Informal description
For any finite set $s$ of type $\alpha$, element $a \in \alpha$, and element $i \in \alpha$, if $i$ is in the finite set obtained by adding $a$ to $s$ (denoted $\text{cons}(a, s, h)$ where $h$ is a proof that $a \notin s$) and $i \neq a$, then $i$ must be in $s$.
Finset.forall_mem_cons theorem
(h : a ∉ s) (p : α → Prop) : (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x
Full source 
theorem forall_mem_cons (h : a ∉ s) (p : α → Prop) :
    (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x := by
  simp only [mem_cons, or_imp, forall_and, forall_eq]
Universal Property of Finite Set Construction via Cons
Informal description
For any element $a$ not in a finite set $s$ (i.e., $a \notin s$) and any predicate $p$ on $\alpha$, the following are equivalent: 1. For all $x$ in the finite set obtained by adding $a$ to $s$ (denoted $\text{cons}(a, s, h)$), the predicate $p(x)$ holds. 2. The predicate $p(a)$ holds and for all $x$ in $s$, the predicate $p(x)$ holds.
Finset.forall_of_forall_cons theorem
{p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ cons a s h → p x) (x) (h : x ∈ s) : p x
Full source 
/-- Useful in proofs by induction. -/
theorem forall_of_forall_cons {p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ cons a s h → p x) (x)
    (h : x ∈ s) : p x :=
  H _ <| mem_cons.2 <| Or.inr h
Predicate Preservation Under Finite Set Construction via Cons
Informal description
For any predicate $p$ on elements of type $\alpha$, if $a$ is not in the finite set $s$ and $p(x)$ holds for all $x$ in the finite set obtained by adding $a$ to $s$ (denoted $\text{cons}(a, s, h)$), then $p(x)$ holds for any $x$ in $s$.
Finset.mk_cons theorem
{s : Multiset α} (h : (a ::ₘ s).Nodup) : (⟨a ::ₘ s, h⟩ : Finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1
Full source 
@[simp]
theorem mk_cons {s : Multiset α} (h : (a ::ₘ s).Nodup) :
    (⟨a ::ₘ s, h⟩ : Finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 :=
  rfl
Construction of Finite Set via Cons from No-Duplicate Multiset
Informal description
Given a multiset $s$ over a type $\alpha$ and a proof $h$ that the multiset $a ::ₘ s$ has no duplicates, the finite set constructed from $a ::ₘ s$ is equal to the disjoint union of the singleton $\{a\}$ and the finite set constructed from $s$, where the proof that $a \notin s$ is derived from $h$.
Finset.cons_empty theorem
(a : α) : cons a ∅ (not_mem_empty _) = { a }
Full source 
@[simp]
theorem cons_empty (a : α) : cons a ∅ (not_mem_empty _) = {a} := rfl
Cons of Element with Empty Set Yields Singleton: $\text{cons}(a, \emptyset, h) = \{a\}$
Informal description
For any element $a$ of type $\alpha$, the finite set obtained by adding $a$ to the empty set (with the proof that $a$ is not in the empty set) is equal to the singleton set $\{a\}$.
Finset.cons_nonempty theorem
(h : a ∉ s) : (cons a s h).Nonempty
Full source 
@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
theorem cons_nonempty (h : a ∉ s) : (cons a s h).Nonempty :=
  ⟨a, mem_cons.2 <| Or.inl rfl⟩
Nonemptiness of Finite Set After Cons Operation
Informal description
For any element $a$ of type $\alpha$ and finite set $s$ of $\alpha$, if $a$ is not in $s$ (with proof $h$), then the finite set $\text{cons}(a, s, h)$ is nonempty.
Finset.cons_ne_empty theorem
(h : a ∉ s) : cons a s h ≠ ∅
Full source 
@[simp] theorem cons_ne_empty (h : a ∉ s) : conscons a s h ≠ ∅ := (cons_nonempty _).ne_empty
Non-emptiness of Cons Operation: $\text{cons}(a, s, h) \neq \emptyset$
Informal description
For any element $a$ of type $\alpha$ and finite set $s$ of $\alpha$, if $a$ is not in $s$ (with proof $h$), then the finite set $\text{cons}(a, s, h)$ is not equal to the empty set $\emptyset$.
Finset.nonempty_mk theorem
{m : Multiset α} {hm} : (⟨m, hm⟩ : Finset α).Nonempty ↔ m ≠ 0
Full source 
@[simp]
theorem nonempty_mk {m : Multiset α} {hm} : (⟨m, hm⟩ : Finset α).Nonempty ↔ m ≠ 0 := by
  induction m using Multiset.induction_on <;> simp
Nonempty Finite Set Characterization via Multiset Non-emptiness
Informal description
For a multiset $m$ of type $\alpha$ with a proof $hm$ that $m$ has no duplicates, the corresponding finite set $\langle m, hm \rangle$ is nonempty if and only if $m$ is not the empty multiset (i.e., $m \neq 0$).
Finset.coe_cons theorem
{a s h} : (@cons α a s h : Set α) = insert a (s : Set α)
Full source 
@[simp]
theorem coe_cons {a s h} : (@cons α a s h : Set α) = insert a (s : Set α) := by
  ext
  simp
Set Correspondence of Finite Set Construction: $\text{cons}(a, s, h) = \{a\} \cup s$
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of $\alpha$, and any proof $h$ that $a \notin s$, the set corresponding to the finite set $\text{cons}(a, s, h)$ is equal to the set obtained by inserting $a$ into the set corresponding to $s$. In symbols, $\text{cons}(a, s, h) = \{a\} \cup s$.
Finset.subset_cons theorem
(h : a ∉ s) : s ⊆ s.cons a h
Full source 
theorem subset_cons (h : a ∉ s) : s ⊆ s.cons a h :=
  Multiset.subset_cons _ _
Subset Property of Finite Set Construction: $s \subseteq s \cup \{a\}$ when $a \notin s$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$ not in $s$ (i.e., $a \notin s$), the set $s$ is a subset of the finite set obtained by adding $a$ to $s$, denoted $s.\text{cons}(a, h)$.
Finset.ssubset_cons theorem
(h : a ∉ s) : s ⊂ s.cons a h
Full source 
theorem ssubset_cons (h : a ∉ s) : s ⊂ s.cons a h :=
  Multiset.ssubset_cons h
Strict Subset Property of Finite Set Construction: $s \subset s \cup \{a\}$ when $a \notin s$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$ not in $s$, the set $s$ is a strict subset of the finite set obtained by adding $a$ to $s$, i.e., $s \subset \{a\} \cup s$.
Finset.cons_subset theorem
{h : a ∉ s} : s.cons a h ⊆ t ↔ a ∈ t ∧ s ⊆ t
Full source 
theorem cons_subset {h : a ∉ s} : s.cons a h ⊆ ts.cons a h ⊆ t ↔ a ∈ t ∧ s ⊆ t :=
  Multiset.cons_subset
Subset Condition for Finite Set Construction: $\{a\} \cup s \subseteq t \leftrightarrow a \in t \land s \subseteq t$
Informal description
For any finite set $s$ of type $\alpha$, element $a \in \alpha$ not in $s$ (i.e., $a \notin s$), and finite set $t$ of $\alpha$, the finite set $\{a\} \cup s$ is a subset of $t$ if and only if $a \in t$ and $s \subseteq t$.
Finset.cons_subset_cons theorem
{hs ht} : s.cons a hs ⊆ t.cons a ht ↔ s ⊆ t
Full source 
@[simp]
theorem cons_subset_cons {hs ht} : s.cons a hs ⊆ t.cons a hts.cons a hs ⊆ t.cons a ht ↔ s ⊆ t := by
  rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
Subset Preservation Under Disjoint Union: $\{a\} \cup s \subseteq \{a\} \cup t \leftrightarrow s \subseteq t$
Informal description
For any finite sets $s$ and $t$ of type $\alpha$, and any element $a \notin s$ (with proof $hs$) and $a \notin t$ (with proof $ht$), the finite set $\{a\} \cup s$ is a subset of $\{a\} \cup t$ if and only if $s$ is a subset of $t$.
Finset.ssubset_iff_exists_cons_subset theorem
: s ⊂ t ↔ ∃ (a : _) (h : a ∉ s), s.cons a h ⊆ t
Full source 
theorem ssubset_iff_exists_cons_subset : s ⊂ ts ⊂ t ↔ ∃ (a : _) (h : a ∉ s), s.cons a h ⊆ t := by
  refine ⟨fun h => ?_, fun ⟨a, ha, h⟩ => ssubset_of_ssubset_of_subset (ssubset_cons _) h⟩
  obtain ⟨a, hs, ht⟩ := not_subset.1 h.2
  exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩
Characterization of Strict Subset via Element Addition: $s \subset t \leftrightarrow \exists a \notin s, \{a\} \cup s \subseteq t$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$, the strict subset relation $s \subset t$ holds if and only if there exists an element $a \in \alpha$ such that $a \notin s$ and the finite set $\{a\} \cup s$ is a subset of $t$.
Finset.cons_swap theorem
(hb : b ∉ s) (ha : a ∉ s.cons b hb) : (s.cons b hb).cons a ha = (s.cons a fun h ↦ ha (mem_cons.mpr (.inr h))).cons b fun h ↦ ha (mem_cons.mpr (.inl ((mem_cons.mp h).elim symm (fun h ↦ False.elim (hb h)))))
Full source 
theorem cons_swap (hb : b ∉ s) (ha : a ∉ s.cons b hb) :
    (s.cons b hb).cons a ha = (s.cons a fun h ↦ ha (mem_cons.mpr (.inr h))).cons b fun h ↦
      ha (mem_cons.mpr (.inl ((mem_cons.mp h).elim symm (fun h ↦ False.elim (hb h))))) :=
  eq_of_veq <| Multiset.cons_swap a b s.val
Commutativity of Finite Set Insertion: $(s \cup \{b\}) \cup \{a\} = (s \cup \{a\}) \cup \{b\}$
Informal description
For any finite set $s$ of type $\alpha$ and elements $a, b \notin s$ (with proofs $hb$ and $ha$ respectively), the finite set obtained by first inserting $b$ into $s$ and then inserting $a$ is equal to the finite set obtained by first inserting $a$ into $s$ and then inserting $b$. More precisely: $$(s \cup \{b\}) \cup \{a\} = (s \cup \{a\}) \cup \{b\}$$
Finset.consPiProd definition
(f : α → Type*) (has : a ∉ s) (x : Π i ∈ cons a s has, f i) : f a × Π i ∈ s, f i
Full source 
/-- Split the added element of cons off a Pi type. -/
@[simps!]
def consPiProd (f : α → Type*) (has : a ∉ s) (x : Π i ∈ cons a s has, f i) : f a × Π i ∈ s, f i :=
  (x a (mem_cons_self a s), fun i hi => x i (mem_cons_of_mem hi))
Splitting a dependent function on a finite set with one added element
Informal description
Given a family of types $f : \alpha \to \text{Type*}$, an element $a \notin s$ (with proof $has$), and a dependent function $x$ defined on $\text{cons}(a, s, has)$, this function splits $x$ into its value at $a$ and the restriction of $x$ to $s$. Specifically, it returns the pair $(x(a), \lambda i \in s, x(i))$, where the first component is the value of $x$ at $a$ (which is automatically in $\text{cons}(a, s, has)$ by self-membership), and the second component is the restriction of $x$ to $s$.
Finset.prodPiCons definition
[DecidableEq α] (f : α → Type*) {a : α} (has : a ∉ s) (x : f a × Π i ∈ s, f i) : (Π i ∈ cons a s has, f i)
Full source 
/-- Combine a product with a pi type to pi of cons. -/
def prodPiCons [DecidableEq α] (f : α → Type*) {a : α} (has : a ∉ s) (x : f a × Π i ∈ s, f i) :
    (Π i ∈ cons a s has, f i) :=
  fun i hi =>
    if h : i = a then cast (congrArg f h.symm) x.1 else x.2 i (mem_of_mem_cons_of_ne hi h)
Dependent function construction on a finite set with one added element
Informal description
Given a family of types $f : \alpha \to \text{Type*}$, an element $a \notin s$ (with proof $has$), and a pair $(x_a, x_s)$ where $x_a \in f(a)$ and $x_s$ is a dependent function on $s$, this function constructs a new dependent function on $\text{cons}(a, s, has)$. The new function evaluates to $x_a$ at $a$ and to $x_s(i)$ for any $i \in s$.
Finset.consPiProdEquiv definition
[DecidableEq α] {s : Finset α} (f : α → Type*) {a : α} (has : a ∉ s) : (Π i ∈ cons a s has, f i) ≃ f a × Π i ∈ s, f i
Full source 
/-- The equivalence between pi types on cons and the product. -/
def consPiProdEquiv [DecidableEq α] {s : Finset α} (f : α → Type*) {a : α} (has : a ∉ s) :
    (Π i ∈ cons a s has, f i) ≃ f a × Π i ∈ s, f i where
  toFun := consPiProd f has
  invFun := prodPiCons f has
  left_inv _ := by
    ext i _
    dsimp only [prodPiCons, consPiProd]
    by_cases h : i = a
    · rw [dif_pos h]
      subst h
      simp_all only [cast_eq]
    · rw [dif_neg h]
  right_inv _ := by
    ext _ hi
    · simp [prodPiCons]
    · simp only [consPiProd_snd]
      exact dif_neg (ne_of_mem_of_not_mem hi has)
Equivalence between dependent functions on a finite set with one added element and a product
Informal description
Given a family of types $f : \alpha \to \text{Type*}$, a finite set $s$ of $\alpha$, an element $a \notin s$ (with proof $has$), there is a natural equivalence between the type of dependent functions $\Pi_{i \in \text{cons}(a, s, has)} f(i)$ and the product type $f(a) \times \Pi_{i \in s} f(i)$. This equivalence splits a dependent function on $\text{cons}(a, s, has)$ into its value at $a$ and its restriction to $s$, and conversely combines such a pair into a dependent function.
Finset.instInsert instance
: Insert α (Finset α)
Full source 
/-- `insert a s` is the set `{a} ∪ s` containing `a` and the elements of `s`. -/
instance : Insert α (Finset α) :=
  ⟨fun a s => ⟨_, s.2.ndinsert a⟩⟩
Insertion Operation for Finite Sets
Informal description
For any type $\alpha$, there is an insertion operation that adds an element $a$ to a finite set $s$ of $\alpha$, resulting in the finite set $\{a\} \cup s$.
Finset.insert_def theorem
(a : α) (s : Finset α) : insert a s = ⟨_, s.2.ndinsert a⟩
Full source 
theorem insert_def (a : α) (s : Finset α) : insert a s = ⟨_, s.2.ndinsert a⟩ :=
  rfl
Definition of Insertion Operation for Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the insertion of $a$ into $s$ is equal to the finite set constructed by adding $a$ to the underlying multiset of $s$ while preserving the no-duplicates property.
Finset.insert_val theorem
(a : α) (s : Finset α) : (insert a s).1 = ndinsert a s.1
Full source 
@[simp]
theorem insert_val (a : α) (s : Finset α) : (insert a s).1 = ndinsert a s.1 :=
  rfl
Underlying Multiset of Insertion Operation for Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the underlying multiset of the finite set obtained by inserting $a$ into $s$ is equal to the insertion of $a$ into the underlying multiset of $s$ while preserving the no-duplicates property.
Finset.insert_val' theorem
(a : α) (s : Finset α) : (insert a s).1 = dedup (a ::ₘ s.1)
Full source 
theorem insert_val' (a : α) (s : Finset α) : (insert a s).1 = dedup (a ::ₘ s.1) := by
  rw [dedup_cons, dedup_eq_self]; rfl
Underlying Multiset of Insertion via Deduplication
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the underlying multiset of the finite set obtained by inserting $a$ into $s$ is equal to the deduplication of the multiset formed by prepending $a$ to the underlying multiset of $s$.
Finset.insert_val_of_not_mem theorem
{a : α} {s : Finset α} (h : a ∉ s) : (insert a s).1 = a ::ₘ s.1
Full source 
theorem insert_val_of_not_mem {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).1 = a ::ₘ s.1 := by
  rw [insert_val, ndinsert_of_not_mem h]
Underlying Multiset of Insertion for Non-Member Element
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, if $a$ is not a member of $s$, then the underlying multiset of the finite set obtained by inserting $a$ into $s$ is equal to the multiset formed by prepending $a$ to the underlying multiset of $s$.
Finset.mem_insert theorem
: a ∈ insert b s ↔ a = b ∨ a ∈ s
Full source 
@[simp]
theorem mem_insert : a ∈ insert b sa ∈ insert b s ↔ a = b ∨ a ∈ s :=
  mem_ndinsert
Membership Criterion for Insertion in Finite Sets
Informal description
For any elements $a, b$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the element $a$ belongs to the finite set obtained by inserting $b$ into $s$ if and only if $a$ equals $b$ or $a$ belongs to $s$. In symbols: $$a \in \text{insert}(b, s) \leftrightarrow a = b \lor a \in s$$
Finset.mem_insert_self theorem
(a : α) (s : Finset α) : a ∈ insert a s
Full source 
theorem mem_insert_self (a : α) (s : Finset α) : a ∈ insert a s :=
  mem_ndinsert_self a s.1
Self-Membership in Inserted Finite Set
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the element $a$ is a member of the finite set obtained by inserting $a$ into $s$, i.e., $a \in \text{insert}(a, s)$.
Finset.mem_insert_of_mem theorem
(h : a ∈ s) : a ∈ insert b s
Full source 
theorem mem_insert_of_mem (h : a ∈ s) : a ∈ insert b s :=
  mem_ndinsert_of_mem h
Membership Preservation Under Insertion in Finite Sets
Informal description
For any element $a$ in a finite set $s$ of type $\alpha$, and for any element $b$ of type $\alpha$, $a$ is also in the finite set obtained by inserting $b$ into $s$, i.e., if $a \in s$ then $a \in \text{insert}(b, s)$.
Finset.mem_of_mem_insert_of_ne theorem
(h : b ∈ insert a s) : b ≠ a → b ∈ s
Full source 
theorem mem_of_mem_insert_of_ne (h : b ∈ insert a s) : b ≠ a → b ∈ s :=
  (mem_insert.1 h).resolve_left
Membership in Inserted Set Implies Membership in Original Set for Distinct Elements
Informal description
For any elements $a, b$ of type $\alpha$ and any finite set $s$ of type $\alpha$, if $b$ belongs to the finite set obtained by inserting $a$ into $s$ and $b \neq a$, then $b$ must belong to $s$. In symbols: $$b \in \text{insert}(a, s) \text{ and } b \neq a \implies b \in s$$
Finset.insert_empty theorem
: insert a (∅ : Finset α) = { a }
Full source 
/-- A version of `LawfulSingleton.insert_empty_eq` that works with `dsimp`. -/
@[simp] lemma insert_empty : insert a (∅ : Finset α) = {a} := rfl
Insertion into Empty Set Yields Singleton: $\text{insert}(a, \emptyset) = \{a\}$
Informal description
For any element $a$ of type $\alpha$, inserting $a$ into the empty finite set results in the singleton finite set $\{a\}$. In symbols: $$\text{insert}(a, \emptyset) = \{a\}$$
Finset.cons_eq_insert theorem
(a s h) : @cons α a s h = insert a s
Full source 
@[simp]
theorem cons_eq_insert (a s h) : @cons α a s h = insert a s :=
  ext fun a => by simp
Equality of Cons and Insert Operations on Finite Sets
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of $\alpha$, and a proof $h$ that $a \notin s$, the finite set $\text{cons}(a, s, h)$ is equal to the finite set obtained by inserting $a$ into $s$, i.e., $\text{cons}(a, s, h) = \text{insert}(a, s)$.
Finset.coe_insert theorem
(a : α) (s : Finset α) : ↑(insert a s) = (insert a s : Set α)
Full source 
@[simp, norm_cast]
theorem coe_insert (a : α) (s : Finset α) : ↑(insert a s) = (insert a s : Set α) :=
  Set.ext fun x => by simp only [mem_coe, mem_insert, Set.mem_insert_iff]
Equality of Underlying Sets After Insertion in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the underlying set of the finite set obtained by inserting $a$ into $s$ is equal to the set obtained by inserting $a$ into the underlying set of $s$. In symbols: $$\text{toSet}(\text{insert } a s) = \{a\} \cup \text{toSet}(s)$$
Finset.mem_insert_coe theorem
{s : Finset α} {x y : α} : x ∈ insert y s ↔ x ∈ insert y (s : Set α)
Full source 
theorem mem_insert_coe {s : Finset α} {x y : α} : x ∈ insert y sx ∈ insert y s ↔ x ∈ insert y (s : Set α) := by
  simp
Membership Preservation under Insertion in Finite Sets and Their Underlying Sets
Informal description
For any finite set $s$ of type $\alpha$ and elements $x, y \in \alpha$, the element $x$ belongs to the finite set obtained by inserting $y$ into $s$ if and only if $x$ belongs to the set obtained by inserting $y$ into the underlying set of $s$. In other words, $x \in \text{insert } y s \leftrightarrow x \in \text{insert } y (s : \text{Set } \alpha)$.
Finset.instLawfulSingleton instance
: LawfulSingleton α (Finset α)
Full source 
instance : LawfulSingleton α (Finset α) :=
  ⟨fun a => by ext; simp⟩
Lawful Singleton Structure on Finite Sets
Informal description
For any type $\alpha$, the singleton operation on finite sets of $\alpha$ satisfies the axioms of a lawful singleton structure. This means that for any element $a \in \alpha$, the singleton set $\{a\}$ behaves as expected with respect to membership and equality.
Finset.insert_eq_of_mem theorem
(h : a ∈ s) : insert a s = s
Full source 
@[simp]
theorem insert_eq_of_mem (h : a ∈ s) : insert a s = s :=
  eq_of_veq <| ndinsert_of_mem h
Insertion of Existing Element Leaves Finite Set Unchanged
Informal description
For any element $a$ in a finite set $s$ of type $\alpha$, the insertion of $a$ into $s$ equals $s$ itself, i.e., $\{a\} \cup s = s$.
Finset.insert_eq_self theorem
: insert a s = s ↔ a ∈ s
Full source 
@[simp]
theorem insert_eq_self : insertinsert a s = s ↔ a ∈ s :=
  ⟨fun h => h ▸ mem_insert_self _ _, insert_eq_of_mem⟩
Insertion Equals Original Set if and only if Element is Already Present
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the insertion of $a$ into $s$ equals $s$ if and only if $a$ is already an element of $s$, i.e., $\{a\} \cup s = s \leftrightarrow a \in s$.
Finset.insert_ne_self theorem
: insert a s ≠ s ↔ a ∉ s
Full source 
theorem insert_ne_self : insertinsert a s ≠ sinsert a s ≠ s ↔ a ∉ s :=
  insert_eq_self.not
Insertion Changes Finite Set if and only if Element is New
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the insertion of $a$ into $s$ is not equal to $s$ if and only if $a$ is not an element of $s$, i.e., $\{a\} \cup s \neq s \leftrightarrow a \notin s$.
Finset.pair_eq_singleton theorem
(a : α) : ({ a, a } : Finset α) = { a }
Full source 
theorem pair_eq_singleton (a : α) : ({a, a} : Finset α) = {a} :=
  insert_eq_of_mem <| mem_singleton_self _
Pair of Identical Elements Equals Singleton: $\{a, a\} = \{a\}$
Informal description
For any element $a$ of type $\alpha$, the finite set $\{a, a\}$ is equal to the singleton finite set $\{a\}$.
Finset.insert_comm theorem
(a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s)
Full source 
theorem insert_comm (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s) :=
  ext fun x => by simp only [mem_insert, or_left_comm]
Commutativity of Insertion in Finite Sets
Informal description
For any elements $a$ and $b$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the finite set obtained by inserting $a$ into the result of inserting $b$ into $s$ is equal to the finite set obtained by inserting $b$ into the result of inserting $a$ into $s$. In other words, $\{a\} \cup (\{b\} \cup s) = \{b\} \cup (\{a\} \cup s)$.
Finset.coe_pair theorem
{a b : α} : (({ a, b } : Finset α) : Set α) = { a, b }
Full source 
@[norm_cast]
theorem coe_pair {a b : α} : (({a, b} : Finset α) : Set α) = {a, b} := by
  ext
  simp
Equality of Finite Pair Set and Set Pair: $\{a, b\} = \{a, b\}$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the underlying set of the finite set $\{a, b\}$ is equal to the set $\{a, b\}$. In symbols: $$\text{toSet}(\{a, b\}) = \{a, b\}$$
Finset.coe_eq_pair theorem
{s : Finset α} {a b : α} : (s : Set α) = { a, b } ↔ s = { a, b }
Full source 
@[simp, norm_cast]
theorem coe_eq_pair {s : Finset α} {a b : α} : (s : Set α) = {a, b} ↔ s = {a, b} := by
  rw [← coe_pair, coe_inj]
Equivalence of Finite Set and Set Pair Equality: $\{a, b\}$
Informal description
For any finite set $s$ of type $\alpha$ and any elements $a, b \in \alpha$, the underlying set of $s$ is equal to $\{a, b\}$ if and only if $s$ is equal to the finite set $\{a, b\}$. In other words, $(s : \text{Set } \alpha) = \{a, b\} \leftrightarrow s = \{a, b\}$.
Finset.pair_comm theorem
(a b : α) : ({ a, b } : Finset α) = { b, a }
Full source 
theorem pair_comm (a b : α) : ({a, b} : Finset α) = {b, a} :=
  insert_comm a b ∅
Commutativity of Finite Set Pair Construction: $\{a, b\} = \{b, a\}$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the finite set $\{a, b\}$ is equal to the finite set $\{b, a\}$.
Finset.insert_idem theorem
(a : α) (s : Finset α) : insert a (insert a s) = insert a s
Full source 
theorem insert_idem (a : α) (s : Finset α) : insert a (insert a s) = insert a s :=
  ext fun x => by simp only [mem_insert, ← or_assoc, or_self_iff]
Idempotence of Insertion in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, inserting $a$ into $s$ twice is the same as inserting it once, i.e., $\text{insert}(a, \text{insert}(a, s)) = \text{insert}(a, s)$.
Finset.insert_nonempty theorem
(a : α) (s : Finset α) : (insert a s).Nonempty
Full source 
@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
theorem insert_nonempty (a : α) (s : Finset α) : (insert a s).Nonempty :=
  ⟨a, mem_insert_self a s⟩
Nonemptiness of Inserted Finite Set
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the set obtained by inserting $a$ into $s$ is nonempty, i.e., $\text{insert}(a, s) \neq \emptyset$.
Finset.insert_ne_empty theorem
(a : α) (s : Finset α) : insert a s ≠ ∅
Full source 
@[simp]
theorem insert_ne_empty (a : α) (s : Finset α) : insertinsert a s ≠ ∅ :=
  (insert_nonempty a s).ne_empty
Non-emptiness of Inserted Finite Set: $\{a\} \cup s \neq \emptyset$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the set obtained by inserting $a$ into $s$ is not equal to the empty set, i.e., $\{a\} \cup s \neq \emptyset$.
Finset.instNonemptyElemToSetInsert instance
(i : α) (s : Finset α) : Nonempty ((insert i s : Finset α) : Set α)
Full source 
instance (i : α) (s : Finset α) : Nonempty ((insert i s : Finset α) : Set α) :=
  (Finset.coe_nonempty.mpr (s.insert_nonempty i)).to_subtype
Nonemptiness of Inserted Finite Set as Subset
Informal description
For any element $i$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the set obtained by inserting $i$ into $s$ is nonempty when viewed as a subset of $\alpha$.
Finset.ne_insert_of_not_mem theorem
(s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t
Full source 
theorem ne_insert_of_not_mem (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t := by
  contrapose! h
  simp [h]
Non-equality of Set and Inserted Set When Element Not Present
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, and an element $a \in \alpha$ such that $a \notin s$, the set $s$ is not equal to the set obtained by inserting $a$ into $t$, i.e., $s \neq t \cup \{a\}$.
Finset.insert_subset_iff theorem
: insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
Full source 
theorem insert_subset_iff : insertinsert a s ⊆ tinsert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by
  simp only [subset_iff, mem_insert, forall_eq, or_imp, forall_and]
Insertion Subset Criterion for Finite Sets
Informal description
For any element $a$ of type $\alpha$ and finite sets $s, t$ of type $\alpha$, the set obtained by inserting $a$ into $s$ is a subset of $t$ if and only if $a$ is an element of $t$ and $s$ is a subset of $t$. In symbols: $$\{a\} \cup s \subseteq t \leftrightarrow a \in t \land s \subseteq t.$$
Finset.insert_subset theorem
(ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t
Full source 
theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insertinsert a s ⊆ t :=
  insert_subset_iff.mpr ⟨ha,hs⟩
Insertion Preserves Subset Property
Informal description
For any element $a$ in a finite set $t$ and any finite subset $s \subseteq t$, the set obtained by inserting $a$ into $s$ is a subset of $t$, i.e., $\{a\} \cup s \subseteq t$.
Finset.subset_insert theorem
(a : α) (s : Finset α) : s ⊆ insert a s
Full source 
@[simp] theorem subset_insert (a : α) (s : Finset α) : s ⊆ insert a s := fun _b => mem_insert_of_mem
Subset Property of Insertion in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the set $s$ is a subset of the set obtained by inserting $a$ into $s$, i.e., $s \subseteq \text{insert}(a, s)$.
Finset.insert_subset_insert theorem
(a : α) {s t : Finset α} (h : s ⊆ t) : insert a s ⊆ insert a t
Full source 
@[gcongr]
theorem insert_subset_insert (a : α) {s t : Finset α} (h : s ⊆ t) : insertinsert a s ⊆ insert a t :=
  insert_subset_iff.2 ⟨mem_insert_self _ _, Subset.trans h (subset_insert _ _)⟩
Insertion Preserves Subset Relation: $\{a\} \cup s \subseteq \{a\} \cup t$ when $s \subseteq t$
Informal description
For any element $a$ of type $\alpha$ and any finite sets $s, t$ of type $\alpha$, if $s \subseteq t$, then the set obtained by inserting $a$ into $s$ is a subset of the set obtained by inserting $a$ into $t$, i.e., $\{a\} \cup s \subseteq \{a\} \cup t$.
Finset.insert_subset_insert_iff theorem
(ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t
Full source 
@[simp] lemma insert_subset_insert_iff (ha : a ∉ s) : insertinsert a s ⊆ insert a tinsert a s ⊆ insert a t ↔ s ⊆ t := by
  simp_rw [← coe_subset]; simp [-coe_subset, ha]
Insertion Preserves Subset Relation Iff: $\{a\} \cup s \subseteq \{a\} \cup t \leftrightarrow s \subseteq t$ when $a \notin s$
Informal description
For any element $a$ not in a finite set $s$ (i.e., $a \notin s$), the inclusion $\{a\} \cup s \subseteq \{a\} \cup t$ holds if and only if $s \subseteq t$.
Finset.insert_inj theorem
(ha : a ∉ s) : insert a s = insert b s ↔ a = b
Full source 
theorem insert_inj (ha : a ∉ s) : insertinsert a s = insert b s ↔ a = b :=
  ⟨fun h => eq_of_mem_insert_of_not_mem (h ▸ mem_insert_self _ _) ha, congr_arg (insert · s)⟩
Injectivity of Insertion for Finite Sets: $\text{insert}(a, s) = \text{insert}(b, s) \leftrightarrow a = b$ when $a \notin s$
Informal description
For any element $a$ not in a finite set $s$ (i.e., $a \notin s$), the equality $\text{insert}(a, s) = \text{insert}(b, s)$ holds if and only if $a = b$.
Finset.insert_inj_on theorem
(s : Finset α) : Set.InjOn (fun a => insert a s) sᶜ
Full source 
theorem insert_inj_on (s : Finset α) : Set.InjOn (fun a => insert a s) sᶜ := fun _ h _ _ =>
  (insert_inj h).1
Injectivity of Insertion on Complement of Finite Set: $\text{insert}(a_1, s) = \text{insert}(a_2, s) \Rightarrow a_1 = a_2$ for $a_1, a_2 \notin s$
Informal description
For any finite set $s$ of type $\alpha$, the function $a \mapsto \text{insert}(a, s)$ is injective on the complement set $s^c$ (i.e., the set of elements not in $s$). In other words, for any $a_1, a_2 \notin s$, if $\text{insert}(a_1, s) = \text{insert}(a_2, s)$, then $a_1 = a_2$.
Finset.ssubset_iff theorem
: s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
Full source 
theorem ssubset_iff : s ⊂ ts ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t := mod_cast @Set.ssubset_iff_insert α s t
Characterization of Strict Subset in Finite Sets via Insertion: $s \subset t \leftrightarrow \exists a \notin s, \{a\} \cup s \subseteq t$
Informal description
For any finite sets $s$ and $t$ of type $\alpha$, $s$ is a strict subset of $t$ if and only if there exists an element $a \notin s$ such that $\{a\} \cup s \subseteq t$.
Finset.ssubset_insert theorem
(h : a ∉ s) : s ⊂ insert a s
Full source 
theorem ssubset_insert (h : a ∉ s) : s ⊂ insert a s :=
  ssubset_iff.mpr ⟨a, h, Subset.rfl⟩
Strict Subset Property of Insertion: $s \subset s \cup \{a\}$ when $a \notin s$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \notin s$, the set $s$ is a strict subset of the set obtained by inserting $a$ into $s$, i.e., $s \subset \{a\} \cup s$.
Finset.cons_induction theorem
{α : Type*} {motive : Finset α → Prop} (empty : motive ∅) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : ∀ s, motive s
Full source 
@[elab_as_elim]
theorem cons_induction {α : Type*} {motive : Finset α → Prop} (empty : motive ∅)
    (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : ∀ s, motive s
  | ⟨s, nd⟩ => by
    induction s using Multiset.induction with
    | empty => exact empty
    | cons a s IH =>
      rw [mk_cons nd]
      exact cons a _ _ (IH _)
Induction Principle for Finite Sets via Disjoint Union
Informal description
Let $\alpha$ be a type and let $motive$ be a predicate on finite subsets of $\alpha$. To prove that $motive(s)$ holds for every finite subset $s$ of $\alpha$, it suffices to: 1. Prove the base case: $motive(\emptyset)$ holds for the empty set. 2. Prove the inductive step: For any element $a \in \alpha$ and any finite subset $s$ of $\alpha$ such that $a \notin s$, if $motive(s)$ holds, then $motive(\{a\} \cup s)$ also holds.
Finset.cons_induction_on theorem
{α : Type*} {motive : Finset α → Prop} (s : Finset α) (empty : motive ∅) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : motive s
Full source 
@[elab_as_elim]
theorem cons_induction_on {α : Type*} {motive : Finset α → Prop} (s : Finset α) (empty : motive ∅)
    (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : motive s :=
  cons_induction empty cons s
Finite Set Induction via Disjoint Union
Informal description
Let $\alpha$ be a type and let $motive$ be a predicate on finite subsets of $\alpha$. For any finite subset $s$ of $\alpha$, to prove that $motive(s)$ holds, it suffices to: 1. Prove the base case: $motive(\emptyset)$ holds for the empty set. 2. Prove the inductive step: For any element $a \in \alpha$ and any finite subset $s'$ of $\alpha$ such that $a \notin s'$, if $motive(s')$ holds, then $motive(\{a\} \cup s')$ also holds.
Finset.induction theorem
{α : Type*} {motive : Finset α → Prop} [DecidableEq α] (empty : motive ∅) (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : ∀ s, motive s
Full source 
@[elab_as_elim]
protected theorem induction {α : Type*} {motive : Finset α → Prop} [DecidableEq α]
    (empty : motive ∅)
    (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : ∀ s, motive s :=
  cons_induction empty fun a s ha => (s.cons_eq_insert a ha).symm ▸ insert a s ha
Induction Principle for Finite Sets via Insertion
Informal description
Let $\alpha$ be a type with decidable equality, and let $motive$ be a predicate on finite subsets of $\alpha$. To prove that $motive(s)$ holds for every finite subset $s$ of $\alpha$, it suffices to: 1. Prove the base case: $motive(\emptyset)$ holds for the empty set. 2. Prove the inductive step: For any element $a \in \alpha$ and any finite subset $s$ of $\alpha$ such that $a \notin s$, if $motive(s)$ holds, then $motive(\{a\} \cup s)$ also holds.
Finset.induction_on theorem
{α : Type*} {motive : Finset α → Prop} [DecidableEq α] (s : Finset α) (empty : motive ∅) (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : motive s
Full source 
/-- To prove a proposition about an arbitrary `Finset α`,
it suffices to prove it for the empty `Finset`,
and to show that if it holds for some `Finset α`,
then it holds for the `Finset` obtained by inserting a new element.
-/
@[elab_as_elim]
protected theorem induction_on {α : Type*} {motive : Finset α → Prop} [DecidableEq α] (s : Finset α)
    (empty : motive ∅)
    (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : motive s :=
  Finset.induction empty insert s
Induction Principle for Finite Sets via Insertion
Informal description
Let $\alpha$ be a type with decidable equality, and let $P$ be a predicate on finite subsets of $\alpha$. To prove that $P(s)$ holds for a given finite subset $s \subseteq \alpha$, it suffices to: 1. Prove the base case: $P(\emptyset)$ holds for the empty set. 2. Prove the inductive step: For any element $a \in \alpha$ and any finite subset $s' \subseteq \alpha$ such that $a \notin s'$, if $P(s')$ holds, then $P(s' \cup \{a\})$ also holds.
Finset.induction_on' theorem
{α : Type*} {motive : Finset α → Prop} [DecidableEq α] (S : Finset α) (empty : motive ∅) (insert : ∀ (a s), a ∈ S → s ⊆ S → a ∉ s → motive s → motive (insert a s)) : motive S
Full source 
/-- To prove a proposition about `S : Finset α`,
it suffices to prove it for the empty `Finset`,
and to show that if it holds for some `Finset α ⊆ S`,
then it holds for the `Finset` obtained by inserting a new element of `S`.
-/
@[elab_as_elim]
theorem induction_on' {α : Type*} {motive : Finset α → Prop} [DecidableEq α] (S : Finset α)
    (empty : motive ∅)
    (insert : ∀ (a s), a ∈ S → s ⊆ S → a ∉ s → motive s → motive (insert a s)) : motive S :=
  @Finset.induction_on α (fun T => T ⊆ S → motive T) _ S (fun _ => empty)
    (fun a s has hqs hs =>
      let ⟨hS, sS⟩ := Finset.insert_subset_iff.1 hs
      insert a s hS sS has (hqs sS))
    (Finset.Subset.refl S)
Induction Principle for Finite Subsets via Insertion of Elements from $S$
Informal description
Let $\alpha$ be a type with decidable equality, and let $P$ be a predicate on finite subsets of $\alpha$. To prove that $P(S)$ holds for a given finite subset $S \subseteq \alpha$, it suffices to: 1. Prove the base case: $P(\emptyset)$ holds for the empty set. 2. Prove the inductive step: For any element $a \in S$ and any finite subset $s \subseteq S$ such that $a \notin s$, if $P(s)$ holds, then $P(s \cup \{a\})$ also holds.
Finset.Nonempty.cons_induction theorem
{α : Type*} {motive : ∀ s : Finset α, s.Nonempty → Prop} (singleton : ∀ a, motive { a } (singleton_nonempty _)) (cons : ∀ a s (h : a ∉ s) (hs), motive s hs → motive (Finset.cons a s h) (cons_nonempty h)) {s : Finset α} (hs : s.Nonempty) : motive s hs
Full source 
/-- To prove a proposition about a nonempty `s : Finset α`, it suffices to show it holds for all
singletons and that if it holds for nonempty `t : Finset α`, then it also holds for the `Finset`
obtained by inserting an element in `t`. -/
@[elab_as_elim]
theorem Nonempty.cons_induction {α : Type*} {motive : ∀ s : Finset α, s.Nonempty → Prop}
    (singleton : ∀ a, motive {a} (singleton_nonempty _))
    (cons : ∀ a s (h : a ∉ s) (hs), motive s hs → motive (Finset.cons a s h) (cons_nonempty h))
    {s : Finset α} (hs : s.Nonempty) : motive s hs := by
  induction s using Finset.cons_induction with
  | empty => exact (not_nonempty_empty hs).elim
  | cons a t ha h =>
    obtain rfl | ht := t.eq_empty_or_nonempty
    · exact singleton a
    · exact cons a t ha ht (h ht)
Induction Principle for Nonempty Finite Sets via Singleton and Disjoint Union
Informal description
Let $\alpha$ be a type and let $P$ be a predicate on nonempty finite subsets of $\alpha$. To prove that $P(s, h_s)$ holds for any nonempty finite subset $s \subseteq \alpha$ (where $h_s$ is a proof that $s$ is nonempty), it suffices to: 1. Prove the base case: For any element $a \in \alpha$, $P(\{a\}, h_{\{a\}})$ holds for the singleton set $\{a\}$ (where $h_{\{a\}}$ is the proof that $\{a\}$ is nonempty). 2. Prove the inductive step: For any element $a \in \alpha$ and any finite subset $s \subseteq \alpha$ such that $a \notin s$ and $s$ is nonempty (with proof $h_s$), if $P(s, h_s)$ holds, then $P(\{a\} \cup s, h_{\{a\} \cup s})$ also holds (where $h_{\{a\} \cup s}$ is the proof that $\{a\} \cup s$ is nonempty).
Finset.Nonempty.exists_cons_eq theorem
{α} {s : Finset α} (hs : s.Nonempty) : ∃ t a ha, cons a t ha = s
Full source 
lemma Nonempty.exists_cons_eq {α} {s : Finset α} (hs : s.Nonempty) : ∃ t a ha, cons a t ha = s :=
  hs.cons_induction (fun a ↦ ⟨∅, a, _, cons_empty _⟩) fun _ _ _ _ _ ↦ ⟨_, _, _, rfl⟩
Decomposition of Nonempty Finite Sets via Disjoint Union with Singleton
Informal description
For any nonempty finite set $s$ of type $\alpha$, there exists a finite set $t \subseteq \alpha$, an element $a \in \alpha$, and a proof $h_a$ that $a \notin t$, such that $s$ can be expressed as the disjoint union $\{a\} \cup t$ via the `cons` operation, i.e., $\text{cons}(a, t, h_a) = s$.
Finset.subtypeInsertEquivOption definition
{t : Finset α} {x : α} (h : x ∉ t) : { i // i ∈ insert x t } ≃ Option { i // i ∈ t }
Full source 
/-- Inserting an element to a finite set is equivalent to the option type. -/
def subtypeInsertEquivOption {t : Finset α} {x : α} (h : x ∉ t) :
    { i // i ∈ insert x t }{ i // i ∈ insert x t } ≃ Option { i // i ∈ t } where
  toFun y := if h : ↑y = x then none else some ⟨y, (mem_insert.mp y.2).resolve_left h⟩
  invFun y := (y.elim ⟨x, mem_insert_self _ _⟩) fun z => ⟨z, mem_insert_of_mem z.2⟩
  left_inv y := by
    by_cases h : ↑y = x
    · simp only [Subtype.ext_iff, h, Option.elim, dif_pos, Subtype.coe_mk]
    · simp only [h, Option.elim, dif_neg, not_false_iff, Subtype.coe_eta, Subtype.coe_mk]
  right_inv := by
    rintro (_ | y)
    · simp only [Option.elim, dif_pos]
    · have : ↑y ≠ x := by
        rintro ⟨⟩
        exact h y.2
      simp only [this, Option.elim, Subtype.eta, dif_neg, not_false_iff, Subtype.coe_mk]
Equivalence between Inserted Finite Set Subtype and Option Type
Informal description
Given a finite set $t$ of type $\alpha$ and an element $x \in \alpha$ not in $t$, the type of elements in the finite set obtained by inserting $x$ into $t$ is equivalent to the option type of elements in $t$. More precisely, there is a bijection between: - The subtype $\{ i \mid i \in \text{insert}(x, t) \}$ (elements in the extended finite set) - The option type $\text{Option} \{ i \mid i \in t \}$ (either `none` representing $x$ or `some` an element of $t$) The bijection maps: - $x$ to `none` - Any other element $y \in t$ to `some y`
Finset.insertPiProd definition
(f : α → Type*) (x : Π i ∈ insert a s, f i) : f a × Π i ∈ s, f i
Full source 
/-- Split the added element of insert off a Pi type. -/
@[simps!]
def insertPiProd (f : α → Type*) (x : Π i ∈ insert a s, f i) : f a × Π i ∈ s, f i :=
  (x a (mem_insert_self a s), fun i hi => x i (mem_insert_of_mem hi))
Decomposition of dependent functions over extended finite sets
Informal description
Given a family of types $f : \alpha \to \text{Type*}$ indexed by elements of a type $\alpha$, and a finite set $s \subseteq \alpha$ with an additional element $a \in \alpha$, the function splits a dependent function $x : \prod_{i \in \text{insert}(a, s)} f(i)$ into a pair consisting of: 1. The value $x(a)$ (since $a \in \text{insert}(a, s)$ by definition) 2. A function $\prod_{i \in s} f(i)$ obtained by restricting $x$ to $s$ In other words, it decomposes a dependent function over the extended finite set $\text{insert}(a, s)$ into its value at the new point $a$ and its restriction to the original set $s$.
Finset.prodPiInsert definition
(f : α → Type*) {a : α} (x : f a × Π i ∈ s, f i) : (Π i ∈ insert a s, f i)
Full source 
/-- Combine a product with a pi type to pi of insert. -/
def prodPiInsert (f : α → Type*) {a : α} (x : f a × Π i ∈ s, f i) : (Π i ∈ insert a s, f i) :=
  fun i hi =>
    if h : i = a then cast (congrArg f h.symm) x.1 else x.2 i (mem_of_mem_insert_of_ne hi h)
Construction of dependent functions over extended finite sets
Informal description
Given a family of types $f : \alpha \to \text{Type*}$ indexed by elements of a type $\alpha$, a finite set $s \subseteq \alpha$, and an element $a \in \alpha$, the function constructs a dependent function $\prod_{i \in \text{insert}(a, s)} f(i)$ from a pair consisting of: 1. A value $x_1 \in f(a)$ 2. A dependent function $x_2 : \prod_{i \in s} f(i)$ The constructed function evaluates to $x_1$ at $i = a$ and to $x_2(i)$ for $i \in s$ with $i \neq a$.
Finset.insertPiProdEquiv definition
[DecidableEq α] {s : Finset α} (f : α → Type*) {a : α} (has : a ∉ s) : (Π i ∈ insert a s, f i) ≃ f a × Π i ∈ s, f i
Full source 
/-- The equivalence between pi types on insert and the product. -/
def insertPiProdEquiv [DecidableEq α] {s : Finset α} (f : α → Type*) {a : α} (has : a ∉ s) :
    (Π i ∈ insert a s, f i) ≃ f a × Π i ∈ s, f i where
  toFun := insertPiProd f
  invFun := prodPiInsert f
  left_inv _ := by
    ext i _
    dsimp only [prodPiInsert, insertPiProd]
    by_cases h : i = a
    · rw [dif_pos h]
      subst h
      simp_all only [cast_eq]
    · rw [dif_neg h]
  right_inv _ := by
    ext _ hi
    · simp [prodPiInsert]
    · simp only [insertPiProd_snd]
      exact dif_neg (ne_of_mem_of_not_mem hi has)
Equivalence between dependent functions on extended finite sets and product types
Informal description
Given a type $\alpha$ with decidable equality, a finite set $s \subseteq \alpha$, a family of types $f : \alpha \to \text{Type*}$, and an element $a \in \alpha$ not in $s$, there is an equivalence between: 1. The dependent product type $\prod_{i \in \text{insert}(a, s)} f(i)$ (functions defined on the finite set $\{a\} \cup s$) 2. The product type $f(a) \times \prod_{i \in s} f(i)$ (a pair consisting of a value at $a$ and a function defined on $s$) The equivalence is given by: - The forward map decomposes a function on $\{a\} \cup s$ into its value at $a$ and its restriction to $s$ - The inverse map combines a value at $a$ with a function on $s$ into a function on $\{a\} \cup s$
Finset.exists_mem_insert theorem
(a : α) (s : Finset α) (p : α → Prop) : (∃ x, x ∈ insert a s ∧ p x) ↔ p a ∨ ∃ x, x ∈ s ∧ p x
Full source 
theorem exists_mem_insert (a : α) (s : Finset α) (p : α → Prop) :
    (∃ x, x ∈ insert a s ∧ p x) ↔ p a ∨ ∃ x, x ∈ s ∧ p x := by
  simp only [mem_insert, or_and_right, exists_or, exists_eq_left]
Existence in Inserted Finite Set
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of type $\alpha$, and any predicate $p$ on $\alpha$, there exists an element $x$ in the set obtained by inserting $a$ into $s$ such that $p(x)$ holds if and only if either $p(a)$ holds or there exists an element $x$ in $s$ such that $p(x)$ holds. In symbols: \[ (\exists x \in \{a\} \cup s,\ p(x)) \leftrightarrow p(a) \lor (\exists x \in s,\ p(x)). \]
Finset.forall_mem_insert theorem
(a : α) (s : Finset α) (p : α → Prop) : (∀ x, x ∈ insert a s → p x) ↔ p a ∧ ∀ x, x ∈ s → p x
Full source 
theorem forall_mem_insert (a : α) (s : Finset α) (p : α → Prop) :
    (∀ x, x ∈ insert a s → p x) ↔ p a ∧ ∀ x, x ∈ s → p x := by
  simp only [mem_insert, or_imp, forall_and, forall_eq]
Universal Quantification over Inserted Finite Set
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of type $\alpha$, and any predicate $p$ on $\alpha$, the following are equivalent: 1. For all $x$ in the set obtained by inserting $a$ into $s$, $p(x)$ holds. 2. $p(a)$ holds and for all $x$ in $s$, $p(x)$ holds.
Finset.forall_of_forall_insert theorem
{p : α → Prop} {a : α} {s : Finset α} (H : ∀ x, x ∈ insert a s → p x) (x) (h : x ∈ s) : p x
Full source 
/-- Useful in proofs by induction. -/
theorem forall_of_forall_insert {p : α → Prop} {a : α} {s : Finset α}
    (H : ∀ x, x ∈ insert a s → p x) (x) (h : x ∈ s) : p x :=
  H _ <| mem_insert_of_mem h
Universal Property Preservation Under Insertion in Finite Sets
Informal description
For any predicate $p$ on a type $\alpha$, any element $a \in \alpha$, and any finite set $s \subseteq \alpha$, if $p(x)$ holds for all $x$ in the set $\{a\} \cup s$, then $p(x)$ holds for all $x \in s$.
Multiset.toFinset_zero theorem
: toFinset (0 : Multiset α) = ∅
Full source 
@[simp]
theorem toFinset_zero : toFinset (0 : Multiset α) = ∅ :=
  rfl
Empty Multiset Maps to Empty Finite Set
Informal description
The finite set corresponding to the empty multiset is the empty set, i.e., $\text{toFinset}(0) = \emptyset$.
Multiset.toFinset_cons theorem
(a : α) (s : Multiset α) : toFinset (a ::ₘ s) = insert a (toFinset s)
Full source 
@[simp]
theorem toFinset_cons (a : α) (s : Multiset α) : toFinset (a ::ₘ s) = insert a (toFinset s) :=
  Finset.eq_of_veq dedup_cons
Conversion of Multiset Cons to Finite Set Insertion
Informal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the finite set corresponding to the multiset obtained by prepending $a$ to $s$ is equal to the finite set obtained by inserting $a$ into the finite set corresponding to $s$. In symbols: $$\text{toFinset}(a ::ₘ s) = \text{insert } a (\text{toFinset } s)$$
Multiset.toFinset_singleton theorem
(a : α) : toFinset ({ a } : Multiset α) = { a }
Full source 
@[simp]
theorem toFinset_singleton (a : α) : toFinset ({a} : Multiset α) = {a} := by
  rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]
Singleton Multiset to Singleton Finite Set Conversion
Informal description
For any element $a$ of type $\alpha$, the finite set corresponding to the singleton multiset $\{a\}$ is equal to the singleton finite set $\{a\}$. In symbols: $$\text{toFinset}(\{a\}) = \{a\}$$
List.toFinset_nil theorem
: toFinset (@nil α) = ∅
Full source 
@[simp]
theorem toFinset_nil : toFinset (@nil α) = ∅ :=
  rfl
Empty List Yields Empty Finite Set
Informal description
The finite set constructed from the empty list is the empty set, i.e., $\mathrm{toFinset}(\mathrm{nil}) = \emptyset$.
List.toFinset_cons theorem
: toFinset (a :: l) = insert a (toFinset l)
Full source 
@[simp]
theorem toFinset_cons : toFinset (a :: l) = insert a (toFinset l) :=
  Finset.eq_of_veq <| by by_cases h : a ∈ l <;> simp [Finset.insert_val', Multiset.dedup_cons, h]
Finite Set Construction from List Cons: $\mathrm{toFinset}(a :: l) = \{a\} \cup \mathrm{toFinset}(l)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the finite set corresponding to the list $a :: l$ is equal to the insertion of $a$ into the finite set corresponding to $l$. That is, $\mathrm{toFinset}(a :: l) = \{a\} \cup \mathrm{toFinset}(l)$.
List.toFinset_replicate_of_ne_zero theorem
{n : ℕ} (hn : n ≠ 0) : (List.replicate n a).toFinset = { a }
Full source 
theorem toFinset_replicate_of_ne_zero {n : ℕ} (hn : n ≠ 0) :
    (List.replicate n a).toFinset = {a} := by
  ext x
  simp [hn, List.mem_replicate]
Finite Set from Replicated List is Singleton: $\mathrm{toFinset}(\mathrm{replicate}\,n\,a) = \{a\}$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$ and any element $a$ of type $\alpha$, the finite set constructed from the list containing $n$ copies of $a$ is equal to the singleton set $\{a\}$. That is, $\mathrm{toFinset}(\mathrm{replicate}\,n\,a) = \{a\}$.
List.toFinset_eq_empty_iff theorem
(l : List α) : l.toFinset = ∅ ↔ l = nil
Full source 
@[simp]
theorem toFinset_eq_empty_iff (l : List α) : l.toFinset = ∅ ↔ l = nil := by
  cases l <;> simp
Empty Finite Set from List iff List is Empty
Informal description
For any list $l$ of elements of type $\alpha$, the finite set constructed from $l$ is empty if and only if $l$ is the empty list. In other words, $\mathrm{toFinset}(l) = \emptyset \leftrightarrow l = []$.
List.toFinset_nonempty_iff theorem
(l : List α) : l.toFinset.Nonempty ↔ l ≠ []
Full source 
@[simp]
theorem toFinset_nonempty_iff (l : List α) : l.toFinset.Nonempty ↔ l ≠ [] := by
  simp [Finset.nonempty_iff_ne_empty]
Nonempty Finite Set from List iff List is Nonempty
Informal description
For any list `l` of elements of type `α`, the finite set obtained from `l` is nonempty if and only if `l` is not the empty list. In other words, $\text{toFinset}(l) \neq \emptyset \leftrightarrow l \neq []$.
Finset.toList_eq_singleton_iff theorem
{a : α} {s : Finset α} : s.toList = [a] ↔ s = { a }
Full source 
@[simp]
theorem toList_eq_singleton_iff {a : α} {s : Finset α} : s.toList = [a] ↔ s = {a} := by
  rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]
List Representation of Singleton Finite Set: $s.\text{toList} = [a] \leftrightarrow s = \{a\}$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the list representation of $s$ is equal to the singleton list $[a]$ if and only if $s$ is equal to the singleton finite set $\{a\}$.
Finset.toList_singleton theorem
: ∀ a, ({ a } : Finset α).toList = [a]
Full source 
@[simp]
theorem toList_singleton : ∀ a, ({a} : Finset α).toList = [a] :=
  Multiset.toList_singleton
List Representation of Singleton Finite Set: $\text{toList}(\{a\}) = [a]$
Informal description
For any element $a$ of type $\alpha$, the list representation of the singleton finite set $\{a\}$ is equal to the singleton list $[a]$.
Finset.toList_cons theorem
{a : α} {s : Finset α} (h : a ∉ s) : (cons a s h).toList ~ a :: s.toList
Full source 
theorem toList_cons {a : α} {s : Finset α} (h : a ∉ s) : (cons a s h).toList ~ a :: s.toList :=
  (List.perm_ext_iff_of_nodup (nodup_toList _) (by simp [h, nodup_toList s])).2 fun x => by
    simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]
List Representation of Cons Operation on Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of $\alpha$ such that $a \notin s$, the list representation of the finite set $\text{cons}(a, s, h)$ is permutation-equivalent to the list obtained by prepending $a$ to the list representation of $s$.
Finset.toList_insert theorem
[DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).toList ~ a :: s.toList
Full source 
theorem toList_insert [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) :
    (insert a s).toList ~ a :: s.toList :=
  cons_eq_insert _ _ h ▸ toList_cons _
List Representation of Insert Operation on Finite Sets: $\text{toList}(\text{insert}(a, s)) \sim a :: \text{toList}(s)$
Informal description
For any type $\alpha$ with decidable equality, given an element $a \in \alpha$ and a finite set $s \subset \alpha$ such that $a \notin s$, the list representation of the finite set $\text{insert}(a, s)$ is permutation-equivalent to the list obtained by prepending $a$ to the list representation of $s$.
Finset.pairwise_cons' theorem
{a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) : Pairwise (r on fun a : s.cons a ha => f a) ↔ Pairwise (r on fun a : s => f a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
Full source 
theorem pairwise_cons' {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) :
    PairwisePairwise (r on fun a : s.cons a ha => f a) ↔
    Pairwise (r on fun a : s => f a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a) := by
  simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert,
    Finset.mem_coe, and_congr_right_iff]
  exact fun _ =>
    ⟨fun h b hb =>
      h b hb <| by
        rintro rfl
        contradiction,
      fun h b hb _ => h b hb⟩
Pairwise Relation Preservation under Finite Set Extension via `cons`
Informal description
Let $s$ be a finite set of type $\alpha$, $a \in \alpha$ such that $a \notin s$, $r$ a binary relation on $\beta$, and $f : \alpha \to \beta$ a function. Then the following are equivalent: 1. The relation $r$ holds pairwise on the image of $f$ over the finite set $\text{cons}(a, s, ha)$ (i.e., for any two distinct elements $x, y \in \text{cons}(a, s, ha)$, we have $r(f(x), f(y))$). 2. The relation $r$ holds pairwise on the image of $f$ over $s$, and for every $b \in s$, both $r(f(a), f(b))$ and $r(f(b), f(a))$ hold.
Finset.pairwise_cons theorem
{a : α} (ha : a ∉ s) (r : α → α → Prop) : Pairwise (r on fun a : s.cons a ha => a) ↔ Pairwise (r on fun a : s => a) ∧ ∀ b ∈ s, r a b ∧ r b a
Full source 
theorem pairwise_cons {a : α} (ha : a ∉ s) (r : α → α → Prop) :
    PairwisePairwise (r on fun a : s.cons a ha => a) ↔
      Pairwise (r on fun a : s => a) ∧ ∀ b ∈ s, r a b ∧ r b a :=
  pairwise_cons' ha r id
Pairwise Relation Characterization for Extended Finite Set via `cons`
Informal description
Let $s$ be a finite set of type $\alpha$, $a \in \alpha$ such that $a \notin s$, and $r$ a binary relation on $\alpha$. Then the following are equivalent: 1. The relation $r$ holds pairwise on the finite set $\text{cons}(a, s, ha)$ (i.e., for any two distinct elements $x, y \in \text{cons}(a, s, ha)$, we have $r(x, y)$). 2. The relation $r$ holds pairwise on $s$, and for every $b \in s$, both $r(a, b)$ and $r(b, a)$ hold.