# mathlib3documentation

data.finset.basic

# Finite sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Terms of type `finset α` are one way of talking about finite subsets of `α` in mathlib. Below, `finset α` is defined as a structure with 2 fields:

1. `val` is a `multiset α` of elements;
2. `nodup` is a proof that `val` has no duplicates.

Finsets in Lean are constructive in that they have an underlying `list` that enumerates their elements. In particular, any function that uses the data of the underlying list cannot depend on its ordering. This is handled on the `multiset` level by multiset API, so in most cases one needn't worry about it explicitly.

Finsets give a basic foundation for defining finite sums and products over types:

1. `∑ i in (s : finset α), f i`;
2. `∏ i in (s : finset α), f i`.

Lean refers to these operations as `big_operator`s. More information can be found in `algebra.big_operators.basic`.

Finsets are directly used to define fintypes in Lean. A `fintype α` instance for a type `α` consists of a universal `finset α` containing every term of `α`, called `univ`. See `data.fintype.basic`. There is also `univ'`, the noncomputable partner to `univ`, which is defined to be `α` as a finset if `α` is finite, and the empty finset otherwise. See `data.fintype.basic`.

`finset.card`, the size of a finset is defined in `data.finset.card`. This is then used to define `fintype.card`, the size of a type.

## Main declarations #

### Main definitions #

• `finset`: Defines a type for the finite subsets of `α`. Constructing a `finset` requires two pieces of data: `val`, a `multiset α` of elements, and `nodup`, a proof that `val` has no duplicates.
• `finset.has_mem`: Defines membership `a ∈ (s : finset α)`.
• `finset.has_coe`: Provides a coercion `s : finset α` to `s : set α`.
• `finset.has_coe_to_sort`: Coerce `s : finset α` to the type of all `x ∈ s`.
• `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.choose`: Given a proof `h` of existence and uniqueness of a certain element satisfying a predicate, `choose s h` returns the element of `s` satisfying that predicate.

### Finset constructions #

• `singleton`: Denoted by `{a}`; the finset consisting of one element.
• `finset.empty`: Denoted by `∅`. The finset associated to any type consisting of no elements.
• `finset.range`: For any `n : ℕ`, `range n` is equal to `{0, 1, ... , n - 1} ⊆ ℕ`. This convention is consistent with other languages and normalizes `card (range n) = n`. Beware, `n` is not in `range n`.
• `finset.attach`: Given `s : finset α`, `attach s` forms a finset of elements of the subtype `{a // a ∈ s}`; in other words, it attaches elements to a proof of membership in the set.

### Finsets from functions #

• `finset.filter`: Given a predicate `p : α → Prop`, `s.filter p` is the finset consisting of those elements in `s` satisfying the predicate `p`.

### The lattice structure on subsets of finsets #

There is a natural lattice structure on the subsets of a set. In Lean, we use lattice notation to talk about things involving unions and intersections. See `order.lattice`. For the lattice structure on finsets, `⊥` is called `bot` with `⊥ = ∅` and `⊤` is called `top` with `⊤ = univ`.

• `finset.has_subset`: Lots of API about lattices, otherwise behaves exactly as one would expect.
• `finset.has_union`: Defines `s ∪ t` (or `s ⊔ t`) as the union of `s` and `t`. See `finset.sup`/`finset.bUnion` for finite unions.
• `finset.has_inter`: Defines `s ∩ t` (or `s ⊓ t`) as the intersection of `s` and `t`. See `finset.inf` for finite intersections.
• `finset.disj_union`: Given a hypothesis `h` which states that finsets `s` and `t` are disjoint, `s.disj_union t h` is the set such that `a ∈ disj_union s t h` iff `a ∈ s` or `a ∈ t`; this does not require decidable equality on the type `α`.

### Operations on two or more finsets #

• `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 `α`.
• `finset.has_union`: see "The lattice structure on subsets of finsets"
• `finset.has_inter`: see "The lattice structure on subsets of finsets"
• `finset.erase`: For any `a : α`, `erase s a` returns `s` with the element `a` removed.
• `finset.has_sdiff`: Defines the set difference `s \ t` for finsets `s` and `t`.
• `finset.product`: Given finsets of `α` and `β`, defines finsets of `α × β`. For arbitrary dependent products, see `data.finset.pi`.
• `finset.bUnion`: Finite unions of finsets; given an indexing function `f : α → finset β` and a `s : finset α`, `s.bUnion f` is the union of all finsets of the form `f a` for `a ∈ s`.
• `finset.bInter`: TODO: Implemement finite intersections.

### Maps constructed using finsets #

• `finset.piecewise`: Given two functions `f`, `g`, `s.piecewise f g` is a function which is equal to `f` on `s` and `g` on the complement.

### Predicates on finsets #

• `disjoint`: defined via the lattice structure on finsets; two sets are disjoint if their intersection is empty.
• `finset.nonempty`: A finset is nonempty if it has elements. This is equivalent to saying `s ≠ ∅`. TODO: Decide on the simp normal form.

### Equivalences between finsets #

• The `data.equiv` files describe a general type of equivalence, so look in there for any lemmas. There is some API for rewriting sums and products from `s` to `t` given that `s ≃ t`. TODO: examples

## Tags #

finite sets, finset

structure finset (α : Type u_4) :
Type u_4

`finset α` is the type of finite sets of elements of `α`. It is implemented as a multiset (a list up to permutation) which has no duplicate elements.

Instances for `finset`
@[protected, instance]
def multiset.can_lift_finset {α : Type u_1} :
Equations
theorem finset.eq_of_veq {α : Type u_1} {s t : finset α} :
s.val = t.val s = t
theorem finset.val_injective {α : Type u_1} :
@[simp]
theorem finset.val_inj {α : Type u_1} {s t : finset α} :
s.val = t.val s = t
@[simp]
theorem finset.dedup_eq_self {α : Type u_1} [decidable_eq α] (s : finset α) :
@[protected, instance]
def finset.has_decidable_eq {α : Type u_1} [decidable_eq α] :
Equations

### membership #

@[protected, instance]
def finset.has_mem {α : Type u_1} :
(finset α)
Equations
theorem finset.mem_def {α : Type u_1} {a : α} {s : finset α} :
a s a s.val
@[simp]
theorem finset.mem_val {α : Type u_1} {a : α} {s : finset α} :
a s.val a s
@[simp]
theorem finset.mem_mk {α : Type u_1} {a : α} {s : multiset α} {nd : s.nodup} :
a {val := s, nodup := nd} a s
@[protected, instance]
def finset.decidable_mem {α : Type u_1} [h : decidable_eq α] (a : α) (s : finset α) :
Equations

### set coercion #

@[protected, instance]
def finset.set.has_coe_t {α : Type u_1} :
has_coe_t (finset α) (set α)

Convert a finset to a set in the natural way.

Equations
@[simp, norm_cast]
theorem finset.mem_coe {α : Type u_1} {a : α} {s : finset α} :
a s a s
@[simp]
theorem finset.set_of_mem {α : Type u_1} {s : finset α} :
{a : α | a s} = s
@[simp]
theorem finset.coe_mem {α : Type u_1} {s : finset α} (x : s) :
x s
@[simp]
theorem finset.mk_coe {α : Type u_1} {s : finset α} (x : s) {h : x s} :
x, h⟩ = x
@[protected, instance]
def finset.decidable_mem' {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
Equations

### extensionality #

theorem finset.ext_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ (a : α), a s₁ a s₂
@[ext]
theorem finset.ext {α : Type u_1} {s₁ s₂ : finset α} :
( (a : α), a s₁ a s₂) s₁ = s₂
@[simp, norm_cast]
theorem finset.coe_inj {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ s₁ = s₂
theorem finset.coe_injective {α : Type u_1} :

### type coercion #

@[protected, instance]
def finset.has_coe_to_sort {α : Type u} :
(Type u)

Coercion from a finset to the corresponding subtype.

Equations
@[protected, simp]
theorem finset.forall_coe {α : Type u_1} (s : finset α) (p : s Prop) :
( (x : s), p x) (x : α) (h : x s), p x, h⟩
@[protected, simp]
theorem finset.exists_coe {α : Type u_1} (s : finset α) (p : s Prop) :
( (x : s), p x) (x : α) (h : x s), p x, h⟩
@[protected, instance]
def finset.pi_finset_coe.can_lift (ι : Type u_1) (α : ι Type u_2) [ne : (i : ι), nonempty (α i)] (s : finset ι) :
can_lift (Π (i : s), α i) (Π (i : ι), α i) (λ (f : Π (i : ι), α i) (i : s), f i) (λ (_x : Π (i : s), α i), true)
Equations
• = (λ (_x : ι), _x s)
@[protected, instance]
def finset.pi_finset_coe.can_lift' (ι : Type u_1) (α : Type u_2) [ne : nonempty α] (s : finset ι) :
can_lift (s α) α) (λ (f : ι α) (i : s), f i) (λ (_x : s α), true)
Equations
• = (λ (_x : ι), α) s
@[protected, instance]
def finset.finset_coe.can_lift {α : Type u_1} (s : finset α) :
s coe (λ (a : α), a s)
Equations
@[simp, norm_cast]
theorem finset.coe_sort_coe {α : Type u_1} (s : finset α) :

### Subset and strict subset relations #

@[protected, instance]
def finset.has_subset {α : Type u_1} :
Equations
@[protected, instance]
def finset.has_ssubset {α : Type u_1} :
Equations
@[protected, instance]
def finset.partial_order {α : Type u_1} :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
theorem finset.subset_def {α : Type u_1} {s t : finset α} :
s t s.val t.val
theorem finset.ssubset_def {α : Type u_1} {s t : finset α} :
s t s t ¬t s
@[simp]
theorem finset.subset.refl {α : Type u_1} (s : finset α) :
s s
@[protected]
theorem finset.subset.rfl {α : Type u_1} {s : finset α} :
s s
@[protected]
theorem finset.subset_of_eq {α : Type u_1} {s t : finset α} (h : s = t) :
s t
theorem finset.subset.trans {α : Type u_1} {s₁ s₂ s₃ : finset α} :
s₁ s₂ s₂ s₃ s₁ s₃
theorem finset.superset.trans {α : Type u_1} {s₁ s₂ s₃ : finset α} :
s₁ s₂ s₂ s₃ s₁ s₃
theorem finset.mem_of_subset {α : Type u_1} {s₁ s₂ : finset α} {a : α} :
s₁ s₂ a s₁ a s₂
theorem finset.not_mem_mono {α : Type u_1} {s t : finset α} (h : s t) {a : α} :
a t a s
theorem finset.subset.antisymm {α : Type u_1} {s₁ s₂ : finset α} (H₁ : s₁ s₂) (H₂ : s₂ s₁) :
s₁ = s₂
theorem finset.subset_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ ⦃x : α⦄, x s₁ x s₂
@[simp, norm_cast]
theorem finset.coe_subset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂
@[simp]
theorem finset.val_le_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁.val s₂.val s₁ s₂
theorem finset.subset.antisymm_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ s₁ s₂ s₂ s₁
theorem finset.not_subset {α : Type u_1} {s t : finset α} :
¬s t (x : α) (H : x s), x t
@[simp]
theorem finset.le_eq_subset {α : Type u_1} :
@[simp]
theorem finset.lt_eq_subset {α : Type u_1} :
theorem finset.le_iff_subset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂
theorem finset.lt_iff_ssubset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ < s₂ s₁ s₂
@[simp, norm_cast]
theorem finset.coe_ssubset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂
@[simp]
theorem finset.val_lt_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁.val < s₂.val s₁ s₂
theorem finset.ssubset_iff_subset_ne {α : Type u_1} {s t : finset α} :
s t s t s t
theorem finset.ssubset_iff_of_subset {α : Type u_1} {s₁ s₂ : finset α} (h : s₁ s₂) :
s₁ s₂ (x : α) (H : x s₂), x s₁
theorem finset.ssubset_of_ssubset_of_subset {α : Type u_1} {s₁ s₂ s₃ : finset α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem finset.ssubset_of_subset_of_ssubset {α : Type u_1} {s₁ s₂ s₃ : finset α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem finset.exists_of_ssubset {α : Type u_1} {s₁ s₂ : finset α} (h : s₁ s₂) :
(x : α) (H : x s₂), x s₁
@[protected, instance]
@[protected, instance]
def finset.is_well_founded_lt {α : Type u_1} :

### Order embedding from `finset α` to `set α`#

def finset.coe_emb {α : Type u_1} :
↪o set α

Coercion to `set α` as an `order_embedding`.

Equations
@[simp]
theorem finset.coe_coe_emb {α : Type u_1} :

### Nonempty #

@[protected]
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
Instances for `finset.nonempty`
@[protected, instance]
def finset.decidable_nonempty {α : Type u_1} {s : finset α} :
Equations
@[simp, norm_cast]
theorem finset.coe_nonempty {α : Type u_1} {s : finset α} :
@[simp]
theorem finset.nonempty_coe_sort {α : Type u_1} {s : finset α} :
theorem finset.nonempty.to_set {α : Type u_1} {s : finset α} :

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

theorem finset.nonempty.coe_sort {α : Type u_1} {s : finset α} :

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

theorem finset.nonempty.bex {α : 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) :
theorem finset.nonempty.forall_const {α : Type u_1} {s : finset α} (h : s.nonempty) {p : Prop} :
( (x : α), x s p) p
theorem finset.nonempty.to_subtype {α : Type u_1} {s : finset α} :
theorem finset.nonempty.to_type {α : Type u_1} {s : finset α} :

### empty #

@[protected]
def finset.empty {α : Type u_1} :

The empty finset

Equations
@[protected, instance]
def finset.has_emptyc {α : Type u_1} :
Equations
@[protected, instance]
def finset.inhabited_finset {α : Type u_1} :
Equations
@[simp]
theorem finset.empty_val {α : Type u_1} :
@[simp]
theorem finset.not_mem_empty {α : Type u_1} (a : α) :
@[simp]
theorem finset.not_nonempty_empty {α : Type u_1} :
@[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) :
theorem finset.nonempty.ne_empty {α : Type u_1} {s : finset α} (h : s.nonempty) :
@[simp]
theorem finset.empty_subset {α : Type u_1} (s : finset α) :
theorem finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : finset α} (H : (x : α), x s) :
s =
theorem finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : finset α} :
s = (x : α), x s
@[simp]
theorem finset.val_eq_zero {α : Type u_1} {s : finset α} :
s.val = 0 s =
theorem finset.subset_empty {α : Type u_1} {s : finset α} :
@[simp]
theorem finset.not_ssubset_empty {α : Type u_1} (s : finset α) :
theorem finset.nonempty_of_ne_empty {α : Type u_1} {s : finset α} (h : s ) :
theorem finset.nonempty_iff_ne_empty {α : Type u_1} {s : finset α} :
@[simp]
theorem finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : finset α} :
theorem finset.eq_empty_or_nonempty {α : Type u_1} (s : finset α) :
@[simp, norm_cast]
theorem finset.coe_empty {α : Type u_1} :
@[simp, norm_cast]
theorem finset.coe_eq_empty {α : Type u_1} {s : finset α} :
@[simp]
theorem finset.is_empty_coe_sort {α : Type u_1} {s : finset α} :
s =
@[protected, instance]
theorem finset.eq_empty_of_is_empty {α : Type u_1} [is_empty α] (s : finset α) :
s =

A `finset` for an empty type is empty.

@[protected, instance]
def finset.order_bot {α : Type u_1} :
Equations
@[simp]
theorem finset.bot_eq_empty {α : Type u_1} :
@[simp]
theorem finset.empty_ssubset {α : Type u_1} {s : finset α} :
theorem finset.nonempty.empty_ssubset {α : Type u_1} {s : finset α} :

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

### singleton #

@[protected, instance]
def finset.has_singleton {α : Type u_1} :
(finset α)

`{a} : finset a` is the set `{a}` containing `a` and nothing else.

This differs from `insert a ∅` in that it does not require a `decidable_eq` instance for `α`.

Equations
@[simp]
theorem finset.singleton_val {α : Type u_1} (a : α) :
{a}.val = {a}
@[simp]
theorem finset.mem_singleton {α : Type u_1} {a b : α} :
b {a} b = a
theorem finset.eq_of_mem_singleton {α : Type u_1} {x y : α} (h : x {y}) :
x = y
theorem finset.not_mem_singleton {α : Type u_1} {a b : α} :
a {b} a b
theorem finset.mem_singleton_self {α : Type u_1} (a : α) :
a {a}
@[simp]
theorem finset.val_eq_singleton_iff {α : Type u_1} {a : α} {s : finset α} :
s.val = {a} s = {a}
theorem finset.singleton_injective {α : Type u_1} :
@[simp]
theorem finset.singleton_inj {α : Type u_1} {a b : α} :
{a} = {b} a = b
@[simp]
theorem finset.singleton_nonempty {α : Type u_1} (a : α) :
@[simp]
theorem finset.singleton_ne_empty {α : Type u_1} (a : α) :
{a}
theorem finset.empty_ssubset_singleton {α : Type u_1} {a : α} :
{a}
@[simp, norm_cast]
theorem finset.coe_singleton {α : Type u_1} (a : α) :
{a} = {a}
@[simp, norm_cast]
theorem finset.coe_eq_singleton {α : Type u_1} {s : finset α} {a : α} :
s = {a} s = {a}
theorem finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : finset α} {a : α} :
s = {a} a s (x : α), x s x = a
theorem finset.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : finset α} {a : α} :
s = {a} s.nonempty (x : α), x s x = a
theorem finset.nonempty.eq_singleton_default {α : Type u_1} [unique α] {s : finset α} :

Alias of the forward direction of `finset.nonempty_iff_eq_singleton_default`.

theorem finset.singleton_iff_unique_mem {α : Type u_1} (s : finset α) :
( (a : α), s = {a}) ∃! (a : α), a s
theorem finset.singleton_subset_set_iff {α : Type u_1} {s : set α} {a : α} :
{a} s a s
@[simp]
theorem finset.singleton_subset_iff {α : Type u_1} {s : finset α} {a : α} :
{a} s a s
@[simp]
theorem finset.subset_singleton_iff {α : Type u_1} {s : finset α} {a : α} :
s {a} s = s = {a}
theorem finset.singleton_subset_singleton {α : Type u_1} {a b : α} :
{a} {b} a = b
@[protected]
theorem finset.nonempty.subset_singleton_iff {α : Type u_1} {s : finset α} {a : α} (h : s.nonempty) :
s {a} s = {a}
theorem finset.subset_singleton_iff' {α : Type u_1} {s : finset α} {a : α} :
s {a} (b : α), b s b = a
@[simp]
theorem finset.ssubset_singleton_iff {α : Type u_1} {s : finset α} {a : α} :
s {a} s =
theorem finset.eq_empty_of_ssubset_singleton {α : Type u_1} {s : finset α} {x : α} (hs : s {x}) :
s =
@[protected, reducible]
def finset.nontrivial {α : Type u_1} (s : finset α) :
Prop

A finset is nontrivial if it has at least two elements.

Equations
@[simp]
theorem finset.not_nontrivial_empty {α : Type u_1} :
@[simp]
theorem finset.not_nontrivial_singleton {α : Type u_1} {a : α} :
theorem finset.nontrivial.ne_singleton {α : Type u_1} {s : finset α} {a : α} (hs : s.nontrivial) :
s {a}
theorem finset.eq_singleton_or_nontrivial {α : Type u_1} {s : finset α} {a : α} (ha : a s) :
s = {a} s.nontrivial
theorem finset.nontrivial_iff_ne_singleton {α : Type u_1} {s : finset α} {a : α} (ha : a s) :
theorem finset.nonempty.exists_eq_singleton_or_nontrivial {α : Type u_1} {s : finset α} :
s.nonempty ( (a : α), s = {a}) s.nontrivial
@[protected, instance]
def finset.nontrivial' {α : Type u_1} [nonempty α] :
@[protected, instance]
def finset.unique {α : Type u_1} [is_empty α] :
Equations

### cons #

def finset.cons {α : Type u_1} (a : α) (s : finset α) (h : a s) :

`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 `decidable_eq α`, and the union is guaranteed to be disjoint.

Equations
@[simp]
theorem finset.mem_cons {α : Type u_1} {s : finset α} {a b : α} {h : a s} :
b s h b = a b s
@[simp]
theorem finset.mem_cons_self {α : Type u_1} (a : α) (s : finset α) {h : a s} :
a s h
@[simp]
theorem finset.cons_val {α : Type u_1} {s : finset α} {a : α} (h : a s) :
s h).val = a ::ₘ s.val
theorem finset.forall_mem_cons {α : Type u_1} {s : finset α} {a : α} (h : a s) (p : α Prop) :
( (x : α), x s h p x) p a (x : α), x s p x
theorem finset.forall_of_forall_cons {α : Type u_1} {s : finset α} {a : α} {p : α Prop} {h : a s} (H : (x : α), x s h p x) (x : α) (h_1 : x s) :
p x

Useful in proofs by induction.

@[simp]
theorem finset.mk_cons {α : Type u_1} {a : α} {s : multiset α} (h : (a ::ₘ s).nodup) :
{val := a ::ₘ s, nodup := h} = {val := s, nodup := _} _
@[simp]
theorem finset.cons_empty {α : Type u_1} (a : α) :
_ = {a}
@[simp]
theorem finset.nonempty_cons {α : Type u_1} {s : finset α} {a : α} (h : a s) :
s h).nonempty
@[simp]
theorem finset.nonempty_mk {α : Type u_1} {m : multiset α} {hm : m.nodup} :
{val := m, nodup := hm}.nonempty m 0
@[simp]
theorem finset.coe_cons {α : Type u_1} {a : α} {s : finset α} {h : a s} :
s h) =
theorem finset.subset_cons {α : Type u_1} {s : finset α} {a : α} (h : a s) :
s s h
theorem finset.ssubset_cons {α : Type u_1} {s : finset α} {a : α} (h : a s) :
s s h
theorem finset.cons_subset {α : Type u_1} {s t : finset α} {a : α} {h : a s} :
s h t a t s t
@[simp]
theorem finset.cons_subset_cons {α : Type u_1} {s t : finset α} {a : α} {hs : a s} {ht : a t} :
s hs t ht s t
theorem finset.ssubset_iff_exists_cons_subset {α : Type u_1} {s t : finset α} :
s t (a : α) (h : a s), s h t

### disjoint #

theorem finset.disjoint_left {α : Type u_1} {s t : finset α} :
t ⦃a : α⦄, a s a t
theorem finset.disjoint_right {α : Type u_1} {s t : finset α} :
t ⦃a : α⦄, a t a s
theorem finset.disjoint_iff_ne {α : Type u_1} {s t : finset α} :
t (a : α), a s (b : α), b t a b
@[simp]
theorem finset.disjoint_val {α : Type u_1} {s t : finset α} :
theorem disjoint.forall_ne_finset {α : Type u_1} {s t : finset α} {a b : α} (h : t) (ha : a s) (hb : b t) :
a b
theorem finset.not_disjoint_iff {α : Type u_1} {s t : finset α} :
¬ t (a : α), a s a t
theorem finset.disjoint_of_subset_left {α : Type u_1} {s t u : finset α} (h : s u) (d : t) :
t
theorem finset.disjoint_of_subset_right {α : Type u_1} {s t u : finset α} (h : t u) (d : u) :
t
@[simp]
theorem finset.disjoint_empty_left {α : Type u_1} (s : finset α) :
@[simp]
theorem finset.disjoint_empty_right {α : Type u_1} (s : finset α) :
@[simp]
theorem finset.disjoint_singleton_left {α : Type u_1} {s : finset α} {a : α} :
disjoint {a} s a s
@[simp]
theorem finset.disjoint_singleton_right {α : Type u_1} {s : finset α} {a : α} :
{a} a s
@[simp]
theorem finset.disjoint_singleton {α : Type u_1} {a b : α} :
disjoint {a} {b} a b
theorem finset.disjoint_self_iff_empty {α : Type u_1} (s : finset α) :
s s =
@[simp, norm_cast]
theorem finset.disjoint_coe {α : Type u_1} {s t : finset α} :
t t
@[simp, norm_cast]
theorem finset.pairwise_disjoint_coe {α : Type u_1} {ι : Type u_2} {s : set ι} {f : ι } :
s.pairwise_disjoint (λ (i : ι), (f i))

### disjoint union #

def finset.disj_union {α : Type u_1} (s t : finset α) (h : t) :

`disj_union s t h` is the set such that `a ∈ disj_union s t h` iff `a ∈ s` or `a ∈ t`. It is the same as `s ∪ t`, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

Equations
@[simp]
theorem finset.mem_disj_union {α : Type u_1} {s t : finset α} {h : t} {a : α} :
a s.disj_union t h a s a t
theorem finset.disj_union_comm {α : Type u_1} (s t : finset α) (h : t) :
s.disj_union t h = t.disj_union s _
@[simp]
theorem finset.empty_disj_union {α : Type u_1} (t : finset α) (h : := disjoint_bot_left) :
h = t
@[simp]
theorem finset.disj_union_empty {α : Type u_1} (s : finset α) (h : := disjoint_bot_right) :
h = s
theorem finset.singleton_disj_union {α : Type u_1} (a : α) (t : finset α) (h : disjoint {a} t) :
{a}.disj_union t h = t _
theorem finset.disj_union_singleton {α : Type u_1} (s : finset α) (a : α) (h : {a}) :
s.disj_union {a} h = s _

### insert #

@[protected, instance]
def finset.has_insert {α : Type u_1} [decidable_eq α] :
(finset α)

`insert a s` is the set `{a} ∪ s` containing `a` and the elements of `s`.

Equations
theorem finset.insert_def {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
= {val := , nodup := _}
@[simp]
theorem finset.insert_val {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s).val =
theorem finset.insert_val' {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s).val = (a ::ₘ s.val).dedup
theorem finset.insert_val_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
s).val = a ::ₘ s.val
@[simp]
theorem finset.mem_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
a a = b a s
theorem finset.mem_insert_self {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
a
theorem finset.mem_insert_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (h : a s) :
a
theorem finset.mem_of_mem_insert_of_ne {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (h : b ) :
b a b s
theorem finset.eq_of_not_mem_of_mem_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (ha : b ) (hb : b s) :
b = a
@[simp]
theorem finset.cons_eq_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) (h : a s) :
s h =
@[simp, norm_cast]
theorem finset.coe_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s) =
theorem finset.mem_insert_coe {α : Type u_1} [decidable_eq α] {s : finset α} {x y : α} :
x x
@[protected, instance]
@[simp]
theorem finset.insert_eq_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (h : a s) :
= s
@[simp]
theorem finset.insert_eq_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
= s a s
theorem finset.insert_ne_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
s a s
@[simp]
theorem finset.pair_eq_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a, a} = {a}
theorem finset.insert.comm {α : Type u_1} [decidable_eq α] (a b : α) (s : finset α) :
=
@[simp, norm_cast]
theorem finset.coe_pair {α : Type u_1} [decidable_eq α] {a b : α} :
{a, b} = {a, b}
@[simp, norm_cast]
theorem finset.coe_eq_pair {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
s = {a, b} s = {a, b}
theorem finset.pair_comm {α : Type u_1} [decidable_eq α] (a b : α) :
{a, b} = {b, a}
@[simp]
theorem finset.insert_idem {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
=
@[simp]
theorem finset.insert_nonempty {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
@[simp]
theorem finset.insert_ne_empty {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

The universe annotation is required for the following instance, possibly this is a bug in Lean. See leanprover.zulipchat.com/#narrow/stream/113488-general/topic/strange.20error.20(universe.20issue.3F)

@[protected, instance]
def finset.has_insert.insert.nonempty {α : Type u} [decidable_eq α] (i : α) (s : finset α) :
theorem finset.ne_insert_of_not_mem {α : Type u_1} [decidable_eq α] (s t : finset α) {a : α} (h : a s) :
s
theorem finset.insert_subset {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
t a t s t
theorem finset.subset_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s
theorem finset.insert_subset_insert {α : Type u_1} [decidable_eq α] (a : α) {s t : finset α} (h : s t) :
theorem finset.insert_inj {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (ha : a s) :
a = b
theorem finset.insert_inj_on {α : Type u_1} [decidable_eq α] (s : finset α) :
set.inj_on (λ (a : α), (s)
theorem finset.ssubset_iff {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t (a : α) (H : a s), t
theorem finset.ssubset_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (h : a s) :
s
theorem finset.cons_induction {α : Type u_1} {p : Prop} (h₁ : p ) (h₂ : ⦃a : α⦄ {s : finset α} (h : a s), p s p s h)) (s : finset α) :
p s
theorem finset.cons_induction_on {α : Type u_1} {p : Prop} (s : finset α) (h₁ : p ) (h₂ : ⦃a : α⦄ {s : finset α} (h : a s), p s p s h)) :
p s
@[protected]
theorem finset.induction {α : Type u_1} {p : Prop} [decidable_eq α] (h₁ : p ) (h₂ : ⦃a : α⦄ {s : finset α}, a s p s p s)) (s : finset α) :
p s
@[protected]
theorem finset.induction_on {α : Type u_1} {p : Prop} [decidable_eq α] (s : finset α) (h₁ : p ) (h₂ : ⦃a : α⦄ {s : finset α}, a s p s p s)) :
p s

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.

theorem finset.induction_on' {α : Type u_1} {p : Prop} [decidable_eq α] (S : finset α) (h₁ : p ) (h₂ : {a : α} {s : finset α}, a S s S a s p s p s)) :
p S

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`.

theorem finset.nonempty.cons_induction {α : Type u_1} {p : Π (s : finset α), s.nonempty Prop} (h₀ : (a : α), p {a} _) (h₁ : ⦃a : α⦄ (s : finset α) (h : a s) (hs : s.nonempty), p s hs p s h) _) {s : finset α} (hs : s.nonempty) :
p s hs

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`.

def finset.subtype_insert_equiv_option {α : Type u_1} [decidable_eq α] {t : finset α} {x : α} (h : x t) :
{i // i option {i // i t}

Inserting an element to a finite set is equivalent to the option type.

Equations
@[simp]
theorem finset.disjoint_insert_left {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
t a t t
@[simp]
theorem finset.disjoint_insert_right {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
t) a s t

### Lattice structure #

@[protected, instance]
def finset.has_union {α : Type u_1} [decidable_eq α] :

`s ∪ t` is the set such that `a ∈ s ∪ t` iff `a ∈ s` or `a ∈ t`.

Equations
@[protected, instance]
def finset.has_inter {α : Type u_1} [decidable_eq α] :

`s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`.

Equations
@[protected, instance]
def finset.lattice {α : Type u_1} [decidable_eq α] :
Equations
@[simp]
theorem finset.sup_eq_union {α : Type u_1} [decidable_eq α] :
@[simp]
theorem finset.inf_eq_inter {α : Type u_1} [decidable_eq α] :
theorem finset.disjoint_iff_inter_eq_empty {α : Type u_1} [decidable_eq α] {s t : finset α} :
t s t =
@[protected, instance]
def finset.decidable_disjoint {α : Type u_1} [decidable_eq α] (U V : finset α) :
Equations

#### union #

theorem finset.union_val_nd {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).val = s.val.ndunion t.val
@[simp]
theorem finset.union_val {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).val = s.val t.val
@[simp]
theorem finset.mem_union {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a s t a s a t
@[simp]
theorem finset.disj_union_eq_union {α : Type u_1} [decidable_eq α] (s t : finset α) (h : t) :
s.disj_union t h = s t
theorem finset.mem_union_left {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (t : finset α) (h : a s) :
a s t
theorem finset.mem_union_right {α : Type u_1} [decidable_eq α] {t : finset α} {a : α} (s : finset α) (h : a t) :
a s t
theorem finset.forall_mem_union {α : Type u_1} [decidable_eq α] {s t : finset α} {p : α Prop} :
( (a : α), a s t p a) ( (a : α), a s p a) (a : α), a t p a
theorem finset.not_mem_union {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a s t a s a t
@[simp, norm_cast]
theorem finset.coe_union {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂
theorem finset.union_subset {α : Type u_1} [decidable_eq α] {s t u : finset α} (hs : s u) :
t u s t u
theorem finset.subset_union_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₁ s₂
theorem finset.subset_union_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₂ s₁ s₂
theorem finset.union_subset_union {α : Type u_1} [decidable_eq α] {s t u v : finset α} (hsu : s u) (htv : t v) :
s t u v
theorem finset.union_subset_union_left {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} (h : s₁ s₂) :
s₁ t s₂ t
theorem finset.union_subset_union_right {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} (h : t₁ t₂) :
s t₁ s t₂
theorem finset.union_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ = s₂ s₁
@[protected, instance]
@[simp]
theorem finset.union_assoc {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ (s₂ s₃)
@[protected, instance]
@[simp]
theorem finset.union_idempotent {α : Type u_1} [decidable_eq α] (s : finset α) :
s s = s
@[protected, instance]
theorem finset.union_subset_left {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : s t u) :
s u
theorem finset.union_subset_right {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : s t u) :
t u
theorem finset.union_left_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = t (s u)
theorem finset.union_right_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s u t
theorem finset.union_self {α : Type u_1} [decidable_eq α] (s : finset α) :
s s = s
@[simp]
theorem finset.union_empty {α : Type u_1} [decidable_eq α] (s : finset α) :
s = s
@[simp]
theorem finset.empty_union {α : Type u_1} [decidable_eq α] (s : finset α) :
s = s
theorem finset.insert_eq {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
= {a} s
@[simp]
theorem finset.insert_union {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
t = (s t)
@[simp]
theorem finset.union_insert {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
s = (s t)
theorem finset.insert_union_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
(s t) =
@[simp]
theorem finset.union_eq_left_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t = s t s
@[simp]
theorem finset.left_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s = s t t s
@[simp]
theorem finset.union_eq_right_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t = t s t
@[simp]
theorem finset.right_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s = t s t s
theorem finset.union_congr_left {α : Type u_1} [decidable_eq α] {s t u : finset α} (ht : t s u) (hu : u s t) :
s t = s u
theorem finset.union_congr_right {α : Type u_1} [decidable_eq α] {s t u : finset α} (hs : s t u) (ht : t s u) :
s u = t u
theorem finset.union_eq_union_iff_left {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t = s u t s u u s t
theorem finset.union_eq_union_iff_right {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s u = t u s t u t s u
@[simp]
theorem finset.disjoint_union_left {α : Type u_1} [decidable_eq α] {s t u : finset α} :
disjoint (s t) u u u
@[simp]
theorem finset.disjoint_union_right {α : Type u_1} [decidable_eq α] {s t u : finset α} :
(t u) t u
theorem finset.induction_on_union {α : Type u_1} [decidable_eq α] (P : Prop) (symm : {a b : finset α}, P a b P b a) (empty_right : {a : finset α}, P a ) (singletons : {a b : α}, P {a} {b}) (union_of : {a b c : finset α}, P a c P b c P (a b) c) (a b : finset α) :
P a b

To prove a relation on pairs of `finset X`, it suffices to show that it is

• symmetric,
• it holds when one of the `finset`s is empty,
• it holds for pairs of singletons,
• if it holds for `[a, c]` and for `[b, c]`, then it holds for `[a ∪ b, c]`.
theorem directed.exists_mem_subset_of_finset_subset_bUnion {α : Type u_1} {ι : Type u_2} [hn : nonempty ι] {f : ι set α} (h : f) {s : finset α} (hs : s (i : ι), f i) :
(i : ι), s f i
theorem directed_on.exists_mem_subset_of_finset_subset_bUnion {α : Type u_1} {ι : Type u_2} {f : ι set α} {c : set ι} (hn : c.nonempty) (hc : directed_on (λ (i j : ι), f i f j) c) {s : finset α} (hs : s (i : ι) (H : i c), f i) :
(i : ι) (H : i c), s f i

#### inter #

theorem finset.inter_val_nd {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂).val = s₁.val.ndinter s₂.val
@[simp]
theorem finset.inter_val {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂).val = s₁.val s₂.val
@[simp]
theorem finset.mem_inter {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ s₂ a s₁ a s₂
theorem finset.mem_of_mem_inter_left {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} (h : a s₁ s₂) :
a s₁
theorem finset.mem_of_mem_inter_right {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} (h : a s₁ s₂) :
a s₂
theorem finset.mem_inter_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ a s₂ a s₁ s₂
theorem finset.inter_subset_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ s₁
theorem finset.inter_subset_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ s₂
theorem finset.subset_inter {α : Type u_1} [decidable_eq α] {s₁ s₂ u : finset α} :
s₁ s₂ s₁ u s₁ s₂ u
@[simp, norm_cast]
theorem finset.coe_inter {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂
@[simp]
theorem finset.union_inter_cancel_left {α : Type u_1} [decidable_eq α] {s t : finset α} :
(s t) s = s
@[simp]
theorem finset.union_inter_cancel_right {α : Type u_1} [decidable_eq α] {s t : finset α} :
(s t) t = t
theorem finset.inter_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ = s₂ s₁
@[simp]
theorem finset.inter_assoc {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ (s₂ s₃)
theorem finset.inter_left_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)
theorem finset.inter_right_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ s₃ s₂
@[simp]
theorem finset.inter_self {α : Type u_1} [decidable_eq α] (s : finset α) :
s s = s
@[simp]
theorem finset.inter_empty {α : Type u_1} [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.empty_inter {α : Type u_1} [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.inter_union_self {α : Type u_1} [decidable_eq α] (s t : finset α) :
s (t s) = s
@[simp]
theorem finset.insert_inter_of_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} (h : a s₂) :
s₂ = (s₁ s₂)
@[simp]
theorem finset.inter_insert_of_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} (h : a s₁) :
s₁ = (s₁ s₂)
@[simp]
theorem finset.insert_inter_of_not_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} (h : a s₂) :
s₂ = s₁ s₂
@[simp]
theorem finset.inter_insert_of_not_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} (h : a s₁) :
s₁ = s₁ s₂
@[simp]
theorem finset.singleton_inter_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (H : a s) :
{a} s = {a}
@[simp]
theorem finset.singleton_inter_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (H : a s) :
{a} s =
@[simp]
theorem finset.inter_singleton_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
s {a} = {a}
@[simp]
theorem finset.inter_singleton_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
s {a} =
theorem finset.inter_subset_inter {α : Type u_1} [decidable_eq α] {x y s t : finset α} (h : x y) (h' : s t) :
x s y t
theorem finset.inter_subset_inter_left {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : t u) :
s t s u
theorem finset.inter_subset_inter_right {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : s t) :
s u t u
theorem finset.inter_subset_union {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t s t
@[protected, instance]
def finset.distrib_lattice {α : Type u_1} [decidable_eq α] :
Equations
@[simp]
theorem finset.union_left_idem {α : Type u_1} [decidable_eq α] (s t : finset α) :
s (s t) = s t
@[simp]
theorem finset.union_right_idem {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t t = s t
@[simp]
theorem finset.inter_left_idem {α : Type u_1} [decidable_eq α] (s t : finset α) :
s (s t) = s t
@[simp]
theorem finset.inter_right_idem {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t t = s t
theorem finset.inter_distrib_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = s t s u
theorem finset.inter_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
(s t) u = s u t u
theorem finset.union_distrib_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = (s t) (s u)
theorem finset.union_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = (s u) (t u)
theorem finset.union_union_distrib_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = s t (s u)
theorem finset.union_union_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s u (t u)
theorem finset.inter_inter_distrib_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = s t (s u)
theorem finset.inter_inter_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = s u (t u)
theorem finset.union_union_union_comm {α : Type u_1} [decidable_eq α] (s t u v : finset α) :
s t (u v) = s u (t v)
theorem finset.inter_inter_inter_comm {α : Type u_1} [decidable_eq α] (s t u v : finset α) :
s t (u v) = s u (t v)
theorem finset.union_eq_empty_iff {α : Type u_1} [decidable_eq α] (A B : finset α) :
A B = A = B =
theorem finset.union_subset_iff {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t u s u t u
theorem finset.subset_inter_iff {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t u s t s u
@[simp]
theorem finset.inter_eq_left_iff_subset {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t = s s t
@[simp]
theorem finset.inter_eq_right_iff_subset {α : Type u_1} [decidable_eq α] (s t : finset α) :
t s = s s t
theorem finset.inter_congr_left {α : Type u_1} [decidable_eq α] {s t u : finset α} (ht : s u t) (hu : s t u) :
s t = s u
theorem finset.inter_congr_right {α : Type u_1} [decidable_eq α] {s t u : finset α} (hs : t u s) (ht : s u t) :
s u = t u
theorem finset.inter_eq_inter_iff_left {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t = s u s u t s t u
theorem finset.inter_eq_inter_iff_right {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s u = t u t u s s u t
theorem finset.ite_subset_union {α : Type u_1} [decidable_eq α] (s s' : finset α) (P : Prop) [decidable P] :
ite P s s' s s'
theorem finset.inter_subset_ite {α : Type u_1} [decidable_eq α] (s s' : finset α) (P : Prop) [decidable P] :
s s' ite P s s'
theorem finset.not_disjoint_iff_nonempty_inter {α : Type u_1} [decidable_eq α] {s t : finset α} :
¬ t (s t).nonempty
theorem finset.nonempty.not_disjoint {α : Type u_1} [decidable_eq α] {s t : finset α} :
(s t).nonempty ¬ t

Alias of the reverse direction of `finset.not_disjoint_iff_nonempty_inter`.

theorem finset.disjoint_or_nonempty_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
t (s t).nonempty

### erase #

def finset.erase {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :

`erase s a` is the set `s - {a}`, that is, the elements of `s` which are not equal to `a`.

Equations
@[simp]
theorem finset.erase_val {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
(s.erase a).val = s.val.erase a
@[simp]
theorem finset.mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
a s.erase b a b a s
theorem finset.not_mem_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
a s.erase a
@[simp, nolint]
theorem finset.erase_empty {α : Type u_1} [decidable_eq α] (a : α) :
@[simp]
theorem finset.erase_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.erase a =
theorem finset.ne_of_mem_erase {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
b s.erase a b a
theorem finset.mem_of_mem_erase {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
b s.erase a b s
theorem finset.mem_erase_of_ne_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
a b a s a s.erase b
theorem finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (hs : b s) (hsa : b s.erase a) :
b = a

An element of `s` that is not an element of `erase s a` must be `a`.

@[simp]
theorem finset.erase_eq_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
s.erase a = s
@[simp]
theorem finset.erase_eq_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
s.erase a = s a s
@[simp]
theorem finset.erase_insert_eq_erase {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
s).erase a = s.erase a
theorem finset.erase_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
s).erase a = s
theorem finset.erase_insert_of_ne {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} (h : a b) :
s).erase b = (s.erase b)
theorem finset.erase_cons_of_ne {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} (ha : a s) (hb : a b) :
s ha).erase b = (s.erase b) _
theorem finset.insert_erase {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
(s.erase a) = s
theorem finset.erase_subset_erase {α : Type u_1} [decidable_eq α] (a : α) {s t : finset α} (h : s t) :
s.erase a t.erase a
theorem finset.erase_subset {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s.erase a s
theorem finset.subset_erase {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :
s t.erase a s t a s
@[simp, norm_cast]
theorem finset.coe_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(s.erase a) = s \ {a}
theorem finset.erase_ssubset {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a s) :
s.erase a s
theorem finset.ssubset_iff_exists_subset_erase {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t (a : α) (H : a t), s t.erase a
theorem finset.erase_ssubset_insert {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
s.erase a
theorem finset.erase_ne_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
s.erase a s a s
theorem finset.erase_cons {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (h : a s) :
s h).erase a = s
theorem finset.erase_idem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
(s.erase a).erase a = s.erase a
theorem finset.erase_right_comm {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
(s.erase a).erase b = (s.erase b).erase a
theorem finset.subset_insert_iff {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :
s s.erase a t
theorem finset.erase_insert_subset {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s).erase a s
theorem finset.insert_erase_subset {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s (s.erase a)
theorem finset.subset_insert_iff_of_not_mem {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (h : a s) :
s s t
theorem finset.erase_subset_iff_of_mem {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (h : a t) :
s.erase a t s t
theorem finset.erase_inj {α : Type u_1} [decidable_eq α] {x y : α} (s : finset α) (hx : x s) :
s.erase x = s.erase y x = y
theorem finset.erase_inj_on {α : Type u_1} [decidable_eq α] (s : finset α) :
s
theorem finset.erase_inj_on' {α : Type u_1} [decidable_eq α] (a : α) :
set.inj_on (λ (s : finset α), s.erase a) {s : | a s}

### sdiff #

@[protected, instance]
def finset.has_sdiff {α : Type u_1} [decidable_eq α] :

`s \ t` is the set consisting of the elements of `s` that are not in `t`.

Equations
@[simp]
theorem finset.sdiff_val {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ \ s₂).val = s₁.val - s₂.val
@[simp]
theorem finset.mem_sdiff {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a s \ t a s a t
@[simp]
theorem finset.inter_sdiff_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ (s₂ \ s₁) =
@[protected, instance]
Equations
theorem finset.not_mem_sdiff_of_mem_right {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (h : a t) :
a s \ t
theorem finset.not_mem_sdiff_of_not_mem_left {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (h : a s) :
a s \ t
theorem finset.union_sdiff_of_subset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) :
s t \ s = t
theorem finset.sdiff_union_of_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} (h : s₁ s₂) :
s₂ \ s₁ s₁ = s₂
theorem finset.inter_sdiff {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t \ u) = s t \ u
@[simp]
theorem finset.sdiff_inter_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₂ \ s₁ s₁ =
@[protected, simp]
theorem finset.sdiff_self {α : Type u_1} [decidable_eq α] (s₁ : finset α) :
s₁ \ s₁ =
theorem finset.sdiff_inter_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s \ (t u) = s \ t s \ u
@[simp]
theorem finset.sdiff_inter_self_left {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ (s t) = s \ t
@[simp]
theorem finset.sdiff_inter_self_right {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ (t s) = s \ t
@[simp]
theorem finset.sdiff_empty {α : Type u_1} [decidable_eq α] {s : finset α} :
s \ = s
theorem finset.sdiff_subset_sdiff {α : Type u_1} [decidable_eq α] {s t u v : finset α} (hst : s t) (hvu : v u) :
s \ u t \ v
@[simp, norm_cast]
theorem finset.coe_sdiff {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ \ s₂) = s₁ \ s₂
@[simp]
theorem finset.union_sdiff_self_eq_union {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t \ s = s t
@[simp]
theorem finset.sdiff_union_self_eq_union {α : Type u_1} [decidable_eq α] {s t : finset α} :
s \ t t = s t
theorem finset.union_sdiff_left {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t) \ s = t \ s
theorem finset.union_sdiff_right {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t) \ t = s \ t
theorem finset.union_sdiff_cancel_left {α : Type u_1} [decidable_eq α] {s t : finset α} (h : t) :
(s t) \ s = t
theorem finset.union_sdiff_cancel_right {α : Type u_1} [decidable_eq α] {s t : finset α} (h : t) :
(s t) \ t = s
theorem finset.union_sdiff_symm {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t \ s = t s \ t
theorem finset.sdiff_union_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ t s t = s
@[simp]
theorem finset.sdiff_idem {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ t \ t = s \ t
theorem finset.subset_sdiff {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s t \ u s t u
@[simp]
theorem finset.sdiff_eq_empty_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s \ t = s t
theorem finset.sdiff_nonempty {α : Type u_1} [decidable_eq α] {s t : finset α} :
(s \ t).nonempty ¬s t
@[simp]
theorem finset.empty_sdiff {α : Type u_1} [decidable_eq α] (s : finset α) :
theorem finset.insert_sdiff_of_not_mem {α : Type u_1} [decidable_eq α] (s : finset α) {t : finset α} {x : α} (h : x t) :
\ t = (s \ t)
theorem finset.insert_sdiff_of_mem {α : Type u_1} [decidable_eq α] {t : finset α} (s : finset α) {x : α} (h : x t) :
\ t = s \ t
@[simp]
theorem finset.insert_sdiff_insert {α : Type u_1} [decidable_eq α] (s t : finset α) (x : α) :
= s \
theorem finset.sdiff_insert_of_not_mem {α : Type u_1} [decidable_eq α] {s : finset α} {x : α} (h : x s) (t : finset α) :
s \ = s \ t
@[simp]
theorem finset.sdiff_subset {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ t s
theorem finset.sdiff_ssubset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : t s) (ht : t.nonempty) :
s \ t s
theorem finset.union_sdiff_distrib {α : Type u_1} [decidable_eq α] (s₁ s₂ t : finset α) :
(s₁ s₂) \ t = s₁ \ t s₂ \ t
theorem finset.sdiff_union_distrib {α : Type u_1} [decidable_eq α] (s t₁ t₂ : finset α) :
s \ (t₁ t₂) = s \ t₁ (s \ t₂)
theorem finset.union_sdiff_self {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t) \ t = s \ t
theorem finset.sdiff_singleton_eq_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s \ {a} = s.erase a
theorem finset.erase_eq {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
s.erase a = s \ {a}
theorem finset.disjoint_erase_comm {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
disjoint (s.erase a) t (t.erase a)
theorem finset.disjoint_of_erase_left {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (ha : a t) (hst : disjoint (s.erase a) t) :
t
theorem finset.disjoint_of_erase_right {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (ha : a s) (hst : (t.erase a)) :
t
@[simp]
theorem finset.inter_erase {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
s t.erase a = (s t).erase a
@[simp]
theorem finset.erase_inter {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
s.erase a t = (s t).erase a
theorem finset.erase_sdiff_comm {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
s.erase a \ t = (s \ t).erase a
theorem finset.insert_union_comm {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
t = s
theorem finset.erase_inter_comm {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
s.erase a t = s t.erase a
theorem finset.erase_union_distrib {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
(s t).erase a = s.erase a t.erase a
theorem finset.insert_inter_distrib {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
(s t) =
theorem finset.erase_sdiff_distrib {α : Type u_1} [decidable_eq α] (s t : finset α) (a : α) :
(s \ t).erase a = s.erase a \ t.erase a
theorem finset.erase_union_of_mem {α : Type u_1} [decidable_eq α] {t : finset α} {a : α} (ha : a t) (s : finset α) :
s.erase a t = s t
theorem finset.union_erase_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (ha : a s) (t : finset α) :
s t.erase a = s t
@[simp]
theorem finset.sdiff_singleton_eq_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (ha : a s) :
s \ {a} = s
theorem finset.sdiff_sdiff_left' {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s \ t \ u = s \ t (s \ u)
theorem finset.sdiff_union_sdiff_cancel {α : Type u_1} [decidable_eq α] {s t u : finset α} (hts : t s) (hut : u t) :
s \ t t \ u = s \ u
theorem finset.sdiff_union_erase_cancel {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (hts : t s) (ha : a t) :
s \ t t.erase a = s.erase a
theorem finset.sdiff_sdiff_eq_sdiff_union {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : u s) :
s \ (t \ u) = s \ t u
theorem finset.sdiff_insert {α : Type u_1} [decidable_eq α] (s t : finset α) (x : α) :
s \ = (s \ t).erase x
theorem finset.sdiff_insert_insert_of_mem_of_not_mem {α : Type u_1} [decidable_eq α] {s t : finset α} {x : α} (hxs : x s) (hxt : x t) :
(s \ = s \ t
theorem finset.sdiff_erase {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} (h : a s) :
s \ t.erase a = (s \ t)
theorem finset.sdiff_erase_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (ha : a s) :
s \ s.erase a = {a}
theorem finset.sdiff_sdiff_self_left {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ (s \ t) = s t
theorem finset.sdiff_sdiff_eq_self {α : Type u_1} [decidable_eq α] {s t : finset α} (h : t s) :
s \ (s \ t) = t
theorem finset.sdiff_eq_sdiff_iff_inter_eq_inter {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
s \ t₁ = s \ t₂ s t₁