# Documentation

Mathlib.Data.Finset.Basic

# Finite sets #

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∑ i in (s : Finset α), f i;
2. ∏ i in (s : Finset α), f i∏ i in (s : Finset α), f i.

Lean refers to these operations as big operators. More information can be found in Mathlib.Algebra.BigOperators.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 Mathlib.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 Mathlib.Data.Fintype.Basic.

Finset.card, the size of a finset is defined in Mathlib.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.instMembershipFinset: Defines membership a ∈ (s : Finset α)∈ (s : Finset α).
• Finset.instCoeTCFinsetSet: Provides a coercion s : Finset α to s : Set α.
• Finset.instCoeSortFinsetType: Coerce s : Finset α to the type of all x ∈ s∈ 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 #

• Finset.instSingletonFinset: 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}∈ s}; in other words, it attaches elements to a proof of membership in the set.

### Finsets from functions #

• Finset.filter: Given a decidable predicate p : α → Prop→ 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 Mathlib.Order.Lattice. For the lattice structure on finsets, ⊥⊥ is called bot with ⊥ = ∅⊥ = ∅∅ and ⊤⊤ is called top with ⊤ = univ⊤ = univ.

• Finset.instHasSubsetFinset: Lots of API about lattices, otherwise behaves as one would expect.
• Finset.instUnionFinset: Defines s ∪ t∪ t (or s ⊔ t⊔ t) as the union of s and t. See Finset.sup/Finset.bunionᵢ for finite unions.
• Finset.instInterFinset: Defines s ∩ t∩ t (or s ⊓ t⊓ t) as the intersection of s and t. See Finset.inf for finite intersections.
• Finset.disjUnion: Given a hypothesis h which states that finsets s and t are disjoint, s.disjUnion t h is the set such that a ∈ disjUnion s t h∈ disjUnion s t h iff a ∈ s∈ s or a ∈ t∈ 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}∪ {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.instUnionFinset: see "The lattice structure on subsets of finsets"
• Finset.instInterFinset: see "The lattice structure on subsets of finsets"
• Finset.erase: For any a : α, erase s a returns s with the element a removed.
• Finset.instSDiffFinset: 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 Mathlib.Data.Finset.Pi.
• Finset.bunionᵢ: Finite unions of finsets; given an indexing function f : α → Finset β→ Finset β and a s : Finset α, s.bunionᵢ f is the union of all finsets of the form f a for a ∈ s∈ 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 Mathlib.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≃ t. TODO: examples

## Tags #

finite sets, finset

structure Finset (α : Type u_1) :
Type u_1
• The underlying multiset

val :
• val contains no duplicates

nodup :

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
instance Multiset.canLiftFinset {α : Type u_1} :
CanLift () () Finset.val Multiset.Nodup
Equations
• Multiset.canLiftFinset = { prf := (_ : ∀ (m : ), y, y.val = m) }
theorem Finset.eq_of_veq {α : Type u_1} {s : } {t : } :
s.val = t.vals = t
@[simp]
theorem Finset.val_inj {α : Type u_1} {s : } {t : } :
s.val = t.val s = t
@[simp]
theorem Finset.dedup_eq_self {α : Type u_1} [inst : ] (s : ) :
Multiset.dedup s.val = s.val
instance Finset.decidableEq {α : Type u_1} [inst : ] :
Equations

### membership #

instance Finset.instMembershipFinset {α : Type u_1} :
Equations
• Finset.instMembershipFinset = { mem := fun a s => a s.val }
theorem Finset.mem_def {α : Type u_1} {a : α} {s : } :
a s a s.val
@[simp]
theorem Finset.mem_val {α : Type u_1} {a : α} {s : } :
a s.val a s
@[simp]
theorem Finset.mem_mk {α : Type u_1} {a : α} {s : } {nd : } :
a { val := s, nodup := nd } a s
instance Finset.decidableMem {α : Type u_1} [_h : ] (a : α) (s : ) :
Equations

### set coercion #

def Finset.toSet {α : Type u_1} (s : ) :
Set α

Convert a finset to a set in the natural way.

Equations
• s = { a | a s }
instance Finset.instCoeTCFinsetSet {α : Type u_1} :
CoeTC () (Set α)

Convert a finset to a set in the natural way.

Equations
• Finset.instCoeTCFinsetSet = { coe := Finset.toSet }
@[simp]
theorem Finset.mem_coe {α : Type u_1} {a : α} {s : } :
a s a s
@[simp]
theorem Finset.setOf_mem {α : Type u_1} {s : } :
{ a | a s } = s
@[simp]
theorem Finset.coe_mem {α : Type u_1} {s : } (x : s) :
x s
theorem Finset.mk_coe {α : Type u_1} {s : } (x : s) {h : x s} :
{ val := x, property := h } = x
instance Finset.decidableMem' {α : Type u_1} [inst : ] (a : α) (s : ) :
Decidable (a s)
Equations

### extensionality #

theorem Finset.ext_iff {α : Type u_1} {s₁ : } {s₂ : } :
s₁ = s₂ ∀ (a : α), a s₁ a s₂
theorem Finset.ext {α : Type u_1} {s₁ : } {s₂ : } :
(∀ (a : α), a s₁ a s₂) → s₁ = s₂
@[simp]
theorem Finset.coe_inj {α : Type u_1} {s₁ : } {s₂ : } :
s₁ = s₂ s₁ = s₂
theorem Finset.coe_injective {α : Type u_1} :
Function.Injective Finset.toSet

### type coercion #

instance Finset.instCoeSortFinsetType {α : Type u} :
CoeSort () (Type u)

Coercion from a finset to the corresponding subtype.

Equations
• Finset.instCoeSortFinsetType = { coe := fun s => { x // x s } }
theorem Finset.forall_coe {α : Type u_1} (s : ) (p : { x // x s }Prop) :
((x : { x // x s }) → p x) (x : α) → (h : x s) → p { val := x, property := h }
theorem Finset.exists_coe {α : Type u_1} (s : ) (p : { x // x s }Prop) :
(x, p x) x h, p { val := x, property := h }
instance Finset.PiFinsetCoe.canLift (ι : Type u_1) (α : ιType u_2) [_ne : ∀ (i : ι), Nonempty (α i)] (s : ) :
CanLift ((i : { x // x s }) → α i) ((i : ι) → α i) (fun f i => f i) fun x => True
Equations
instance Finset.PiFinsetCoe.canLift' (ι : Type u_1) (α : Type u_2) [_ne : ] (s : ) :
CanLift ({ x // x s }α) (ια) (fun f i => f i) fun x => True
Equations
instance Finset.FinsetCoe.canLift {α : Type u_1} (s : ) :
CanLift α { x // x s } Subtype.val fun a => a s
Equations
• = { prf := (_ : ∀ (a : α), a sy, y = a) }
@[simp]
theorem Finset.coe_sort_coe {α : Type u_1} (s : ) :
s = { x // x s }

### Subset and strict subset relations #

instance Finset.instHasSubsetFinset {α : Type u_1} :
Equations
• Finset.instHasSubsetFinset = { Subset := fun s t => ∀ ⦃a : α⦄, a sa t }
Equations
• Finset.instHasSSubsetFinset = { SSubset := fun s t => s t ¬t s }
instance Finset.partialOrder {α : Type u_1} :
Equations
instance Finset.instIsReflFinsetSubsetInstHasSubsetFinset {α : Type u_1} :
IsRefl () fun x x_1 => x x_1
Equations
instance Finset.instIsTransFinsetSubsetInstHasSubsetFinset {α : Type u_1} :
IsTrans () fun x x_1 => x x_1
Equations
instance Finset.instIsAntisymmFinsetSubsetInstHasSubsetFinset {α : Type u_1} :
IsAntisymm () fun x x_1 => x x_1
Equations
instance Finset.instIsIrreflFinsetSSubsetInstHasSSubsetFinset {α : Type u_1} :
IsIrrefl () fun x x_1 => x x_1
Equations
instance Finset.instIsTransFinsetSSubsetInstHasSSubsetFinset {α : Type u_1} :
IsTrans () fun x x_1 => x x_1
Equations
instance Finset.instIsAsymmFinsetSSubsetInstHasSSubsetFinset {α : Type u_1} :
IsAsymm () fun x x_1 => x x_1
Equations
Equations
• Finset.instIsNonstrictStrictOrderFinsetSubsetInstHasSubsetFinsetSSubsetInstHasSSubsetFinset = { right_iff_left_not_left := (_ : ∀ (x x_1 : ), x x_1 x x_1) }
theorem Finset.subset_def {α : Type u_1} {s : } {t : } :
s t s.val t.val
theorem Finset.ssubset_def {α : Type u_1} {s : } {t : } :
s t s t ¬t s
@[simp]
theorem Finset.Subset.refl {α : Type u_1} (s : ) :
s s
theorem Finset.Subset.rfl {α : Type u_1} {s : } :
s s
theorem Finset.subset_of_eq {α : Type u_1} {s : } {t : } (h : s = t) :
s t
theorem Finset.Subset.trans {α : Type u_1} {s₁ : } {s₂ : } {s₃ : } :
s₁ s₂s₂ s₃s₁ s₃
theorem Finset.Superset.trans {α : Type u_1} {s₁ : } {s₂ : } {s₃ : } :
s₁ s₂s₂ s₃s₁ s₃
theorem Finset.mem_of_subset {α : Type u_1} {s₁ : } {s₂ : } {a : α} :
s₁ s₂a s₁a s₂
theorem Finset.not_mem_mono {α : Type u_1} {s : } {t : } (h : s t) {a : α} :
¬a t¬a s
theorem Finset.Subset.antisymm {α : Type u_1} {s₁ : } {s₂ : } (H₁ : s₁ s₂) (H₂ : s₂ s₁) :
s₁ = s₂
theorem Finset.subset_iff {α : Type u_1} {s₁ : } {s₂ : } :
s₁ s₂ ∀ ⦃x : α⦄, x s₁x s₂
@[simp]
theorem Finset.coe_subset {α : Type u_1} {s₁ : } {s₂ : } :
s₁ s₂ s₁ s₂
@[simp]
theorem Finset.val_le_iff {α : Type u_1} {s₁ : } {s₂ : } :
s₁.val s₂.val s₁ s₂
theorem Finset.Subset.antisymm_iff {α : Type u_1} {s₁ : } {s₂ : } :
s₁ = s₂ s₁ s₂ s₂ s₁
theorem Finset.not_subset {α : Type u_1} {s : } {t : } :
¬s t x, x s ¬x t
@[simp]
theorem Finset.le_eq_subset {α : Type u_1} :
(fun x x_1 => x x_1) = fun x x_1 => x x_1
@[simp]
theorem Finset.lt_eq_subset {α : Type u_1} :
(fun x x_1 => x < x_1) = fun x x_1 => x x_1
theorem Finset.le_iff_subset {α : Type u_1} {s₁ : } {s₂ : } :
s₁ s₂ s₁ s₂
theorem Finset.lt_iff_ssubset {α : Type u_1} {s₁ : } {s₂ : } :
s₁ < s₂ s₁ s₂
@[simp]
theorem Finset.coe_ssubset {α : Type u_1} {s₁ : } {s₂ : } :
s₁ s₂ s₁ s₂
@[simp]
theorem Finset.val_lt_iff {α : Type u_1} {s₁ : } {s₂ : } :
s₁.val < s₂.val s₁ s₂
theorem Finset.ssubset_iff_subset_ne {α : Type u_1} {s : } {t : } :
s t s t s t
theorem Finset.ssubset_iff_of_subset {α : Type u_1} {s₁ : } {s₂ : } (h : s₁ s₂) :
s₁ s₂ x, x s₂ ¬x s₁
theorem Finset.ssubset_of_ssubset_of_subset {α : Type u_1} {s₁ : } {s₂ : } {s₃ : } (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem Finset.ssubset_of_subset_of_ssubset {α : Type u_1} {s₁ : } {s₂ : } {s₃ : } (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem Finset.exists_of_ssubset {α : Type u_1} {s₁ : } {s₂ : } (h : s₁ s₂) :
x, x s₂ ¬x s₁
instance Finset.isWellFounded_ssubset {α : Type u_1} :
IsWellFounded () fun x x_1 => x x_1
Equations
instance Finset.wellFoundedLT {α : Type u_1} :
Equations

### Order embedding from Finset α to Set α#

def Finset.coeEmb {α : Type u_1} :
↪o Set α

Coercion to Set α as an OrderEmbedding.

Equations
• Finset.coeEmb = { toEmbedding := { toFun := Finset.toSet, inj' := (_ : Function.Injective Finset.toSet) }, map_rel_iff' := (_ : ∀ {a b : }, a b a b) }
@[simp]
theorem Finset.coe_coeEmb {α : Type u_1} :
Finset.coeEmb.toEmbedding = Finset.toSet

### Nonempty #

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

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∃ x, x ∈ s∈ s or s ≠ ∅≠ ∅∅ as it gives access to a nice API thanks to the dot notation.

Equations
instance Finset.decidableNonempty {α : Type u_1} {s : } :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.coe_nonempty {α : Type u_1} {s : } :
theorem Finset.nonempty_coe_sort {α : Type u_1} {s : } :
Nonempty { x // x s }
theorem Finset.Nonempty.to_set {α : Type u_1} {s : } :

Alias of the reverse direction of Finset.coe_nonempty.

theorem Finset.Nonempty.coe_sort {α : Type u_1} {s : } :
Nonempty { x // x s }

Alias of the reverse direction of Finset.nonempty_coe_sort.

theorem Finset.Nonempty.bex {α : Type u_1} {s : } (h : ) :
x, x s
theorem Finset.Nonempty.mono {α : Type u_1} {s : } {t : } (hst : s t) (hs : ) :
theorem Finset.Nonempty.forall_const {α : Type u_1} {s : } (h : ) {p : Prop} :
((x : α) → x sp) p
theorem Finset.Nonempty.to_subtype {α : Type u_1} {s : } :
Nonempty { x // x s }
theorem Finset.Nonempty.to_type {α : Type u_1} {s : } :

### empty #

def Finset.empty {α : Type u_1} :

The empty finset

Equations
• Finset.empty = { val := 0, nodup := (_ : ) }
Equations
• Finset.instEmptyCollectionFinset = { emptyCollection := Finset.empty }
instance Finset.inhabitedFinset {α : Type u_1} :
Equations
• Finset.inhabitedFinset = { default := }
@[simp]
theorem Finset.empty_val {α : Type u_1} :
.val = 0
@[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 : } (h : a s) :
theorem Finset.Nonempty.ne_empty {α : Type u_1} {s : } (h : ) :
@[simp]
theorem Finset.empty_subset {α : Type u_1} (s : ) :
theorem Finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : } (H : ∀ (x : α), ¬x s) :
s =
theorem Finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : } :
s = ∀ (x : α), ¬x s
@[simp]
theorem Finset.val_eq_zero {α : Type u_1} {s : } :
s.val = 0 s =
theorem Finset.subset_empty {α : Type u_1} {s : } :
@[simp]
theorem Finset.not_ssubset_empty {α : Type u_1} (s : ) :
theorem Finset.nonempty_of_ne_empty {α : Type u_1} {s : } (h : s ) :
theorem Finset.nonempty_iff_ne_empty {α : Type u_1} {s : } :
@[simp]
theorem Finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : } :
s =
theorem Finset.eq_empty_or_nonempty {α : Type u_1} (s : ) :
s =
@[simp]
theorem Finset.coe_empty {α : Type u_1} :
=
@[simp]
theorem Finset.coe_eq_empty {α : Type u_1} {s : } :
s = s =
theorem Finset.isEmpty_coe_sort {α : Type u_1} {s : } :
IsEmpty { x // x s } s =
Equations
• One or more equations did not get rendered due to their size.
theorem Finset.eq_empty_of_isEmpty {α : Type u_1} [inst : ] (s : ) :
s =

A Finset for an empty type is empty.

Equations
• Finset.instOrderBotFinsetToLEToPreorderPartialOrder = OrderBot.mk (_ : ∀ (s : ), s)
@[simp]
theorem Finset.bot_eq_empty {α : Type u_1} :
@[simp]
theorem Finset.empty_ssubset {α : Type u_1} {s : } :
theorem Finset.Nonempty.empty_ssubset {α : Type u_1} {s : } :
s

Alias of the reverse direction of Finset.empty_ssubset.

### singleton #

instance Finset.instSingletonFinset {α : Type u_1} :
Singleton α ()

{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 α.

Equations
• Finset.instSingletonFinset = { singleton := fun a => { val := {a}, nodup := (_ : ) } }
@[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 : } :
s.val = {a} s = {a}
@[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]
theorem Finset.coe_singleton {α : Type u_1} (a : α) :
{a} = {a}
@[simp]
theorem Finset.coe_eq_singleton {α : Type u_1} {s : } {a : α} :
s = {a} s = {a}
theorem Finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : } {a : α} :
s = {a} a s ∀ (x : α), x sx = a
theorem Finset.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : } {a : α} :
s = {a} ∀ (x : α), x sx = a
theorem Finset.nonempty_iff_eq_singleton_default {α : Type u_1} [inst : ] {s : } :
s = {default}
theorem Finset.Nonempty.eq_singleton_default {α : Type u_1} [inst : ] {s : } :
s = {default}

Alias of the forward direction of Finset.nonempty_iff_eq_singleton_default.

theorem Finset.singleton_iff_unique_mem {α : Type u_1} (s : ) :
(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 : } {a : α} :
{a} s a s
@[simp]
theorem Finset.subset_singleton_iff {α : Type u_1} {s : } {a : α} :
s {a} s = s = {a}
theorem Finset.singleton_subset_singleton {α : Type u_1} {a : α} {b : α} :
{a} {b} a = b
theorem Finset.Nonempty.subset_singleton_iff {α : Type u_1} {s : } {a : α} (h : ) :
s {a} s = {a}
theorem Finset.subset_singleton_iff' {α : Type u_1} {s : } {a : α} :
s {a} ∀ (b : α), b sb = a
@[simp]
theorem Finset.ssubset_singleton_iff {α : Type u_1} {s : } {a : α} :
s {a} s =
theorem Finset.eq_empty_of_ssubset_singleton {α : Type u_1} {s : } {x : α} (hs : s {x}) :
s =
theorem Finset.eq_singleton_or_nontrivial {α : Type u_1} {s : } {a : α} (ha : a s) :
s = {a}
theorem Finset.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u_1} {s : } :
(a, s = {a})
instance Finset.instNontrivialFinset {α : Type u_1} [inst : ] :
Equations
instance Finset.instUniqueFinset {α : Type u_1} [inst : ] :
Equations
• Finset.instUniqueFinset = { toInhabited := { default := }, uniq := (_ : ∀ (x : ), x = ) }

### cons #

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

cons a s h is the set {a} ∪ s∪ 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.

Equations
@[simp]
theorem Finset.mem_cons {α : Type u_1} {s : } {a : α} {b : α} {h : ¬a s} :
b Finset.cons a s h b = a b s
theorem Finset.mem_cons_self {α : Type u_1} (a : α) (s : ) {h : ¬a s} :
@[simp]
theorem Finset.cons_val {α : Type u_1} {s : } {a : α} (h : ¬a s) :
(Finset.cons a s h).val = a ::ₘ s.val
theorem Finset.forall_mem_cons {α : Type u_1} {s : } {a : α} (h : ¬a s) (p : αProp) :
((x : α) → x Finset.cons a s hp x) p a ((x : α) → x sp x)
@[simp]
theorem Finset.mk_cons {α : Type u_1} {a : α} {s : } (h : Multiset.Nodup (a ::ₘ s)) :
{ val := a ::ₘ s, nodup := h } = Finset.cons a { val := s, nodup := (_ : ) } (_ : ¬a s)
@[simp]
theorem Finset.nonempty_cons {α : Type u_1} {s : } {a : α} (h : ¬a s) :
@[simp]
theorem Finset.nonempty_mk {α : Type u_1} {m : } {hm : } :
Finset.Nonempty { val := m, nodup := hm } m 0
@[simp]
theorem Finset.coe_cons {α : Type u_1} {a : α} {s : } {h : ¬a s} :
↑(Finset.cons a s h) = insert a s
theorem Finset.subset_cons {α : Type u_1} {s : } {a : α} (h : ¬a s) :
theorem Finset.ssubset_cons {α : Type u_1} {s : } {a : α} (h : ¬a s) :
theorem Finset.cons_subset {α : Type u_1} {s : } {t : } {a : α} {h : ¬a s} :
Finset.cons a s h t a t s t
@[simp]
theorem Finset.cons_subset_cons {α : Type u_1} {s : } {t : } {a : α} {hs : ¬a s} {ht : ¬a t} :
Finset.cons a s hs Finset.cons a t ht s t
theorem Finset.ssubset_iff_exists_cons_subset {α : Type u_1} {s : } {t : } :
s t a h, Finset.cons a s h t

### disjoint #

theorem Finset.disjoint_left {α : Type u_1} {s : } {t : } :
Disjoint s t ∀ ⦃a : α⦄, a s¬a t
theorem Finset.disjoint_right {α : Type u_1} {s : } {t : } :
Disjoint s t ∀ ⦃a : α⦄, a t¬a s
theorem Finset.disjoint_iff_ne {α : Type u_1} {s : } {t : } :
Disjoint s t ∀ (a : α), a s∀ (b : α), b ta b
@[simp]
theorem Finset.disjoint_val {α : Type u_1} {s : } {t : } :
theorem Disjoint.forall_ne_finset {α : Type u_1} {s : } {t : } {a : α} {b : α} (h : Disjoint s t) (ha : a s) (hb : b t) :
a b
theorem Finset.not_disjoint_iff {α : Type u_1} {s : } {t : } :
¬Disjoint s t a, a s a t
theorem Finset.disjoint_of_subset_left {α : Type u_1} {s : } {t : } {u : } (h : s u) (d : Disjoint u t) :
theorem Finset.disjoint_of_subset_right {α : Type u_1} {s : } {t : } {u : } (h : t u) (d : Disjoint s u) :
@[simp]
theorem Finset.disjoint_empty_left {α : Type u_1} (s : ) :
@[simp]
theorem Finset.disjoint_empty_right {α : Type u_1} (s : ) :
@[simp]
theorem Finset.disjoint_singleton_left {α : Type u_1} {s : } {a : α} :
Disjoint {a} s ¬a s
@[simp]
theorem Finset.disjoint_singleton_right {α : Type u_1} {s : } {a : α} :
Disjoint s {a} ¬a s
theorem Finset.disjoint_singleton {α : Type u_1} {a : α} {b : α} :
Disjoint {a} {b} a b
@[simp]
theorem Finset.disjoint_coe {α : Type u_1} {s : } {t : } :
Disjoint s t Disjoint s t
@[simp]
theorem Finset.pairwiseDisjoint_coe {α : Type u_2} {ι : Type u_1} {s : Set ι} {f : ι} :
(Set.PairwiseDisjoint s fun i => ↑(f i))

### disjoint union #

def Finset.disjUnion {α : Type u_1} (s : ) (t : ) (h : Disjoint s t) :

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

Equations
@[simp]
theorem Finset.mem_disjUnion {α : Type u_1} {s : } {t : } {h : Disjoint s t} {a : α} :
a a s a t
theorem Finset.disjUnion_comm {α : Type u_1} (s : ) (t : ) (h : Disjoint s t) :
= Finset.disjUnion t s (_ : Disjoint t s)
@[simp]
theorem Finset.empty_disjUnion {α : Type u_1} (t : ) (h : optParam () (_ : )) :
= t
@[simp]
theorem Finset.disjUnion_empty {α : Type u_1} (s : ) (h : optParam () (_ : )) :
= s
theorem Finset.singleton_disjUnion {α : Type u_1} (a : α) (t : ) (h : Disjoint {a} t) :
Finset.disjUnion {a} t h = Finset.cons a t (_ : ¬a t)
theorem Finset.disjUnion_singleton {α : Type u_1} (s : ) (a : α) (h : Disjoint s {a}) :
Finset.disjUnion s {a} h = Finset.cons a s (_ : ¬a s)

### insert #

instance Finset.instInsertFinset {α : Type u_1} [inst : ] :
Insert α ()

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

Equations
theorem Finset.insert_def {α : Type u_1} [inst : ] (a : α) (s : ) :
insert a s = { val := Multiset.ndinsert a s.val, nodup := (_ : Multiset.Nodup (Multiset.ndinsert a s.val)) }
@[simp]
theorem Finset.insert_val {α : Type u_1} [inst : ] (a : α) (s : ) :
(insert a s).val = Multiset.ndinsert a s.val
theorem Finset.insert_val' {α : Type u_1} [inst : ] (a : α) (s : ) :
(insert a s).val = Multiset.dedup (a ::ₘ s.val)
theorem Finset.insert_val_of_not_mem {α : Type u_1} [inst : ] {a : α} {s : } (h : ¬a s) :
(insert a s).val = a ::ₘ s.val
@[simp]
theorem Finset.mem_insert {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
a insert b s a = b a s
theorem Finset.mem_insert_self {α : Type u_1} [inst : ] (a : α) (s : ) :
a insert a s
theorem Finset.mem_insert_of_mem {α : Type u_1} [inst : ] {s : } {a : α} {b : α} (h : a s) :
a insert b s
theorem Finset.mem_of_mem_insert_of_ne {α : Type u_1} [inst : ] {s : } {a : α} {b : α} (h : b insert a s) :
b ab s
theorem Finset.eq_of_not_mem_of_mem_insert {α : Type u_1} [inst : ] {s : } {a : α} {b : α} (ha : b insert a s) (hb : ¬b s) :
b = a
@[simp]
theorem Finset.cons_eq_insert {α : Type u_1} [inst : ] (a : α) (s : ) (h : ¬a s) :
Finset.cons a s h = insert a s
@[simp]
theorem Finset.coe_insert {α : Type u_1} [inst : ] (a : α) (s : ) :
↑(insert a s) = insert a s
theorem Finset.mem_insert_coe {α : Type u_1} [inst : ] {s : } {x : α} {y : α} :
x insert y s x insert y s
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.insert_eq_of_mem {α : Type u_1} [inst : ] {s : } {a : α} (h : a s) :
insert a s = s
@[simp]
theorem Finset.insert_eq_self {α : Type u_1} [inst : ] {s : } {a : α} :
insert a s = s a s
theorem Finset.insert_ne_self {α : Type u_1} [inst : ] {s : } {a : α} :
insert a s s ¬a s
theorem Finset.pair_eq_singleton {α : Type u_1} [inst : ] (a : α) :
{a, a} = {a}
theorem Finset.Insert.comm {α : Type u_1} [inst : ] (a : α) (b : α) (s : ) :
insert a (insert b s) = insert b (insert a s)
theorem Finset.coe_pair {α : Type u_1} [inst : ] {a : α} {b : α} :
{a, b} = {a, b}
@[simp]
theorem Finset.coe_eq_pair {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
s = {a, b} s = {a, b}
theorem Finset.pair_comm {α : Type u_1} [inst : ] (a : α) (b : α) :
{a, b} = {b, a}
theorem Finset.insert_idem {α : Type u_1} [inst : ] (a : α) (s : ) :
insert a (insert a s) = insert a s
@[simp]
theorem Finset.insert_nonempty {α : Type u_1} [inst : ] (a : α) (s : ) :
@[simp]
theorem Finset.insert_ne_empty {α : Type u_1} [inst : ] (a : α) (s : ) :
instance Finset.instNonemptyElemToSetInsertFinsetInstInsertFinset {α : Type u_1} [inst : ] (i : α) (s : ) :
Nonempty ↑(insert i s)
Equations
theorem Finset.ne_insert_of_not_mem {α : Type u_1} [inst : ] (s : ) (t : ) {a : α} (h : ¬a s) :
s insert a t
theorem Finset.insert_subset {α : Type u_1} [inst : ] {s : } {t : } {a : α} :
insert a s t a t s t
theorem Finset.subset_insert {α : Type u_1} [inst : ] (a : α) (s : ) :
s insert a s
theorem Finset.insert_subset_insert {α : Type u_1} [inst : ] (a : α) {s : } {t : } (h : s t) :
insert a s insert a t
theorem Finset.insert_inj {α : Type u_1} [inst : ] {s : } {a : α} {b : α} (ha : ¬a s) :
insert a s = insert b s a = b
theorem Finset.insert_inj_on {α : Type u_1} [inst : ] (s : ) :
Set.InjOn (fun a => insert a s) (s)
theorem Finset.ssubset_iff {α : Type u_1} [inst : ] {s : } {t : } :
s t a x, insert a s t
theorem Finset.ssubset_insert {α : Type u_1} [inst : ] {s : } {a : α} (h : ¬a s) :
s insert a s
theorem Finset.cons_induction {α : Type u_1} {p : Prop} (h₁ : p ) (h₂ : a : α⦄ → {s : } → (h : ¬a s) → p sp (Finset.cons a s h)) (s : ) :
p s
theorem Finset.cons_induction_on {α : Type u_1} {p : Prop} (s : ) (h₁ : p ) (h₂ : a : α⦄ → {s : } → (h : ¬a s) → p sp (Finset.cons a s h)) :
p s
theorem Finset.induction {α : Type u_1} {p : Prop} [inst : ] (h₁ : p ) (h₂ : a : α⦄ → {s : } → ¬a sp sp (insert a s)) (s : ) :
p s
theorem Finset.induction_on {α : Type u_1} {p : Prop} [inst : ] (s : ) (empty : p ) (insert : a : α⦄ → {s : } → ¬a sp sp (insert a 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} [inst : ] (S : ) (h₁ : p ) (h₂ : {a : α} → {s : } → a Ss S¬a sp sp (insert a 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⊆ 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 : ) → } (h₀ : (a : α) → p {a} (_ : )) (h₁ : a : α⦄ → (s : ) → (h : ¬a s) → (hs : ) → p s hsp (Finset.cons a s h) (_ : Finset.Nonempty (Finset.cons a s h))) {s : } (hs : ) :
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.subtypeInsertEquivOption {α : Type u_1} [inst : ] {t : } {x : α} (h : ¬x t) :
{ i // i insert x t } Option { i // i t }

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.disjoint_insert_left {α : Type u_1} [inst : ] {s : } {t : } {a : α} :
@[simp]
theorem Finset.disjoint_insert_right {α : Type u_1} [inst : ] {s : } {t : } {a : α} :

### Lattice structure #

instance Finset.instUnionFinset {α : Type u_1} [inst : ] :

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

Equations
instance Finset.instInterFinset {α : Type u_1} [inst : ] :

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

Equations
instance Finset.instLatticeFinset {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.sup_eq_union {α : Type u_1} [inst : ] :
Sup.sup = Union.union
@[simp]
theorem Finset.inf_eq_inter {α : Type u_1} [inst : ] :
Inf.inf = Inter.inter
theorem Finset.disjoint_iff_inter_eq_empty {α : Type u_1} [inst : ] {s : } {t : } :
Disjoint s t s t =
instance Finset.decidableDisjoint {α : Type u_1} [inst : ] (U : ) (V : ) :
Equations

#### union #

theorem Finset.union_val_nd {α : Type u_1} [inst : ] (s : ) (t : ) :
(s t).val = Multiset.ndunion s.val t.val
@[simp]
theorem Finset.union_val {α : Type u_1} [inst : ] (s : ) (t : ) :
(s t).val = s.val t.val
@[simp]
theorem Finset.mem_union {α : Type u_1} [inst : ] {s : } {t : } {a : α} :
a s t a s a t
@[simp]
theorem Finset.disjUnion_eq_union {α : Type u_1} [inst : ] (s : ) (t : ) (h : Disjoint s t) :
= s t
theorem Finset.mem_union_left {α : Type u_1} [inst : ] {s : } {a : α} (t : ) (h : a s) :
a s t
theorem Finset.mem_union_right {α : Type u_1} [inst : ] {t : } {a : α} (s : ) (h : a t) :
a s t
theorem Finset.forall_mem_union {α : Type u_1} [inst : ] {s : } {t : } {p : αProp} :
((a : α) → a s tp a) ((a : α) → a sp a) ((a : α) → a tp a)
theorem Finset.not_mem_union {α : Type u_1} [inst : ] {s : } {t : } {a : α} :
¬a s t ¬a s ¬a t
@[simp]
theorem Finset.coe_union {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
↑(s₁ s₂) = s₁ s₂
theorem Finset.union_subset {α : Type u_1} [inst : ] {s : } {t : } {u : } (hs : s u) :
t us t u
theorem Finset.subset_union_left {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
s₁ s₁ s₂
theorem Finset.subset_union_right {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
s₂ s₁ s₂
theorem Finset.union_subset_union {α : Type u_1} [inst : ] {s : } {t : } {u : } {v : } (hsu : s u) (htv : t v) :
s t u v
theorem Finset.union_comm {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
s₁ s₂ = s₂ s₁
instance Finset.instIsCommutativeFinsetUnionInstUnionFinset {α : Type u_1} [inst : ] :
IsCommutative () fun x x_1 => x x_1
Equations
@[simp]
theorem Finset.union_assoc {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) (s₃ : ) :
s₁ s₂ s₃ = s₁ (s₂ s₃)
instance Finset.instIsAssociativeFinsetUnionInstUnionFinset {α : Type u_1} [inst : ] :
IsAssociative () fun x x_1 => x x_1
Equations
@[simp]
theorem Finset.union_idempotent {α : Type u_1} [inst : ] (s : ) :
s s = s
instance Finset.instIsIdempotentFinsetUnionInstUnionFinset {α : Type u_1} [inst : ] :
IsIdempotent () fun x x_1 => x x_1
Equations
theorem Finset.union_subset_left {α : Type u_1} [inst : ] {s : } {t : } {u : } (h : s t u) :
s u
theorem Finset.union_subset_right {α : Type u_1} [inst : ] {s : } {t : } {u : } (h : s t u) :
t u
theorem Finset.union_left_comm {α : Type u_1} [inst : ] (s : ) (t : ) (u : ) :
s (t u) = t (s u)
theorem Finset.union_right_comm {α : Type u_1} [inst : ] (s : ) (t : ) (u : ) :
s t u = s u t
theorem Finset.union_self {α : Type u_1} [inst : ] (s : ) :
s s = s
@[simp]
theorem Finset.union_empty {α : Type u_1} [inst : ] (s : ) :
s = s
@[simp]
theorem Finset.empty_union {α : Type u_1} [inst : ] (s : ) :
s = s
theorem Finset.insert_eq {α : Type u_1} [inst : ] (a : α) (s : ) :
insert a s = {a} s
@[simp]
theorem Finset.insert_union {α : Type u_1} [inst : ] (a : α) (s : ) (t : ) :
insert a s t = insert a (s t)
@[simp]
theorem Finset.union_insert {α : Type u_1} [inst : ] (a : α) (s : ) (t : ) :
s insert a t = insert a (s t)
theorem Finset.insert_union_distrib {α : Type u_1} [inst : ] (a : α) (s : ) (t : ) :
insert a (s t) = insert a s insert a t
@[simp]
theorem Finset.union_eq_left_iff_subset {α : Type u_1} [inst : ] {s : } {t : } :
s t = s t s
@[simp]
theorem Finset.left_eq_union_iff_subset {α : Type u_1} [inst : ] {s : } {t : } :
s = s t t s
@[simp]
theorem Finset.union_eq_right_iff_subset {α : Type u_1} [inst : ] {s : } {t : } :
s t = t s t
@[simp]
theorem Finset.right_eq_union_iff_subset {α : Type u_1} [inst : ] {s : } {t : } :
s = t s t s
theorem Finset.union_congr_left {α : Type u_1} [inst : ] {s : } {t : } {u : } (ht : t s u) (hu : u s t) :
s t = s u
theorem Finset.union_congr_right {α : Type u_1} [inst : ] {s : } {t : } {u : } (hs : s t u) (ht : t s u) :
s u = t u
theorem Finset.union_eq_union_iff_left {α : Type u_1} [inst : ] {s : } {t : } {u : } :
s t = s u t s u u s t
theorem Finset.union_eq_union_iff_right {α : Type u_1} [inst : ] {s : } {t : } {u : } :
s u = t u s t u t s u
@[simp]
theorem Finset.disjoint_union_left {α : Type u_1} [inst : ] {s : } {t : } {u : } :
@[simp]
theorem Finset.disjoint_union_right {α : Type u_1} [inst : ] {s : } {t : } {u : } :
theorem Finset.induction_on_union {α : Type u_1} [inst : ] (P : Prop) (symm : {a b : } → P a bP b a) (empty_right : {a : } → P a ) (singletons : {a b : α} → P {a} {b}) (union_of : {a b c : } → P a cP b cP (a b) c) (a : ) (b : ) :
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 Finsets 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]∪ b, c].
theorem Directed.exists_mem_subset_of_finset_subset_bunionᵢ {α : Type u_1} {ι : Type u_2} [hn : ] {f : ιSet α} (h : Directed (fun x x_1 => x x_1) f) {s : } (hs : s Set.unionᵢ fun i => f i) :
i, s f i
theorem DirectedOn.exists_mem_subset_of_finset_subset_bunionᵢ {α : Type u_1} {ι : Type u_2} {f : ιSet α} {c : Set ι} (hn : ) (hc : DirectedOn (fun i j => f i f j) c) {s : } (hs : s Set.unionᵢ fun i => Set.unionᵢ fun h => f i) :
i, i c s f i

#### inter #

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

Alias of the reverse direction of Finset.not_disjoint_iff_nonempty_inter.

theorem Finset.disjoint_or_nonempty_inter {α : Type u_1} [inst : ] (s : ) (t : ) :

### erase #

def Finset.erase {α : Type u_1} [inst : ] (s : ) (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} [inst : ] (s : ) (a : α) :
().val = Multiset.erase s.val a
@[simp]
theorem Finset.mem_erase {α : Type u_1} [inst : ] {a : α} {b : α} {s : } :
a a b a s
theorem Finset.not_mem_erase {α : Type u_1} [inst : ] (a : α) (s : ) :
@[simp]
theorem Finset.erase_empty {α : Type u_1} [inst : ] (a : α) :
@[simp]
theorem Finset.erase_singleton {α : Type u_1} [inst : ] (a : α) :
theorem Finset.ne_of_mem_erase {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
b b a
theorem Finset.mem_of_mem_erase {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
b b s
theorem Finset.mem_erase_of_ne_of_mem {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
a ba sa
theorem Finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [inst : ] {s : } {a : α} {b : α} (hs : b s) (hsa : ¬b ) :
b = a

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

@[simp]
theorem Finset.erase_eq_of_not_mem {α : Type u_1} [inst : ] {a : α} {s : } (h : ¬a s) :
= s
@[simp]
theorem Finset.erase_eq_self {α : Type u_1} [inst : ] {s : } {a : α} :
= s ¬a s
@[simp]
theorem Finset.erase_insert_eq_erase {α : Type u_1} [inst : ] (s : ) (a : α) :
theorem Finset.erase_insert {α : Type u_1} [inst : ] {a : α} {s : } (h : ¬a s) :
theorem Finset.erase_insert_of_ne {α : Type u_1} [inst : ] {a : α} {b : α} {s : } (h : a b) :
theorem Finset.erase_cons_of_ne {α : Type u_1} [inst : ] {a : α} {b : α} {s : } (ha : ¬a s) (hb : a b) :
Finset.erase (Finset.cons a s ha) b = Finset.cons a () fun h => ha (_ : a s.val)
theorem Finset.insert_erase {α : Type u_1} [inst : ] {a : α} {s : } (h : a s) :
insert a () = s
theorem Finset.erase_subset_erase {α : Type u_1} [inst : ] (a : α) {s : } {t : } (h : s t) :
theorem Finset.erase_subset {α : Type u_1} [inst : ] (a : α) (s : ) :
s
theorem Finset.subset_erase {α : Type u_1} [inst : ] {a : α} {s : } {t : } :
s s t ¬a s
@[simp]
theorem Finset.coe_erase {α : Type u_1} [inst : ] (a : α) (s : ) :
↑() = s \ {a}
theorem Finset.erase_ssubset {α : Type u_1} [inst : ] {a : α} {s : } (h : a s) :
s
theorem Finset.ssubset_iff_exists_subset_erase {α : Type u_1} [inst : ] {s : } {t : } :
s t a, a t s
theorem Finset.erase_ssubset_insert {α : Type u_1} [inst : ] (s : ) (a : α) :
insert a s
theorem Finset.erase_ne_self {α : Type u_1} [inst : ] {s : } {a : α} :
s a s
theorem Finset.erase_cons {α : Type u_1} [inst : ] {s : } {a : α} (h : ¬a s) :
theorem Finset.erase_idem {α : Type u_1} [inst : ] {a : α} {s : } :
theorem Finset.erase_right_comm {α : Type u_1} [inst : ] {a : α} {b : α} {s : } :
theorem Finset.subset_insert_iff {α : Type u_1} [inst : ] {a : α} {s : } {t : } :
s insert a t t
theorem Finset.erase_insert_subset {α : Type u_1} [inst : ] (a : α) (s : ) :
theorem Finset.insert_erase_subset {α : Type u_1} [inst : ] (a : α) (s : ) :
s insert a ()
theorem Finset.subset_insert_iff_of_not_mem {α : Type u_1} [inst : ] {s : } {t : } {a : α} (h : ¬a s) :
s insert a t s t
theorem Finset.erase_subset_iff_of_mem {α : Type u_1} [inst : ] {s : } {t : } {a : α} (h : a t) :
t s t
theorem Finset.erase_inj {α : Type u_1} [inst : ] {x : α} {y : α} (s : ) (hx : x s) :
= x = y
theorem Finset.erase_injOn {α : Type u_1} [inst : ] (s : ) :
Set.InjOn () s
theorem Finset.erase_injOn' {α : Type u_1} [inst : ] (a : α) :
Set.InjOn (fun s => ) { s | a s }

### sdiff #

instance Finset.instSDiffFinset {α : Type u_1} [inst : ] :

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

Equations
• Finset.instSDiffFinset = { sdiff := fun s₁ s₂ => { val := s₁.val - s₂.val, nodup := (_ : Multiset.Nodup (s₁.val - s₂.val)) } }
@[simp]
theorem Finset.sdiff_val {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
(s₁ \ s₂).val = s₁.val - s₂.val
@[simp]
theorem Finset.mem_sdiff {α : Type u_1} [inst : ] {s : } {t : } {a : α} :
a s \ t a s ¬a t
@[simp]
theorem Finset.inter_sdiff_self {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
s₁ (s₂ \ s₁) =
instance Finset.instGeneralizedBooleanAlgebraFinset {α : Type u_1} [inst : ] :
Equations
theorem Finset.not_mem_sdiff_of_mem_right {α : Type u_1} [inst : ] {s : } {t : } {a : α} (h : a t) :
¬a s \ t
theorem Finset.not_mem_sdiff_of_not_mem_left {α : Type u_1} [inst : ] {s : } {t : } {a : α} (h : ¬a s) :
¬a s \ t
theorem Finset.union_sdiff_of_subset {α : Type u_1} [inst : ] {s : } {t : } (h : s t) :
s t \ s = t
theorem Finset.sdiff_union_of_subset {α : Type u_1} [inst : ] {s₁ : } {s₂ : } (h : s₁ s₂) :
s₂ \ s₁ s₁ = s₂
theorem Finset.inter_sdiff {α : Type u_1} [inst : ] (s : ) (t : ) (u : ) :
s (t \ u) = (s t) \ u
@[simp]
theorem Finset.sdiff_inter_self {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
s₂ \ s₁ s₁ =
theorem Finset.sdiff_self {α : Type u_1} [inst : ] (s₁ : ) :
s₁ \ s₁ =
theorem Finset.sdiff_inter_distrib_right {α : Type u_1} [inst : ] (s : ) (t : ) (u : ) :
s \ (t u) = s \ t s \ u
@[simp]
theorem Finset.sdiff_inter_self_left {α : Type u_1} [inst : ] (s : ) (t : ) :
s \ (s t) = s \ t
@[simp]
theorem Finset.sdiff_inter_self_right {α : Type u_1} [inst : ] (s : ) (t : ) :
s \ (t s) = s \ t
@[simp]
theorem Finset.sdiff_empty {α : Type u_1} [inst : ] {s : } :
s \ = s
theorem Finset.sdiff_subset_sdiff {α : Type u_1} [inst : ] {s : } {t : } {u : } {v : } (hst : s t) (hvu : v u) :
s \ u t \ v
@[simp]
theorem Finset.coe_sdiff {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) :
↑(s₁ \ s₂) = s₁ \ s₂
@[simp]
theorem Finset.union_sdiff_self_eq_union {α : Type u_1} [inst : ] {s : } {t : } :
s t \ s = s t
@[simp]
theorem Finset.sdiff_union_self_eq_union {α : Type u_1} [inst : ] {s : } {t : } :
s \ t t = s t
theorem Finset.union_sdiff_left {α : Type u_1} [inst : ] (s : ) (t : ) :
(s t) \ s = t \ s
theorem Finset.union_sdiff_right {α : Type u_1} [inst : ] (s : ) (t : ) :
(s t) \ t = s \ t
theorem Finset.union_sdiff_symm {α : Type u_1} [inst : ] {s : } {t : } :
s t \ s = t s \ t
theorem Finset.sdiff_union_inter {α : Type u_1} [inst : ] (s : ) (t : ) :
s \ t s t = s
theorem Finset.sdiff_idem {α : Type u_1} [inst : ] (s : ) (t : ) :
(s \ t) \ t = s \ t
theorem Finset.subset_sdiff {α : Type u_1} [inst : ] {s : } {t : } {u : } :
s t \ u s t Disjoint s u
@[simp]
theorem Finset.sdiff_eq_empty_iff_subset {α : Type u_1} [inst : ] {s : } {t : } :
s \ t = s t
theorem Finset.sdiff_nonempty {α : Type u_1} [inst : ] {s : } {t : } :
@[simp]
theorem Finset.empty_sdiff {α : Type u_1} [inst : ] (s : ) :
theorem Finset.insert_sdiff_of_not_mem {α : Type u_1} [inst : ] (s : ) {t : } {x : α} (h : ¬x t) :
insert x s \ t = insert x (s \ t)
theorem Finset.insert_sdiff_of_mem {α : Type u_1} [inst : ] {t : } (s : ) {x : α} (h : x t) :
insert x s \ t = s \ t
@[simp]
theorem Finset.insert_sdiff_insert {α : Type u_1} [inst : ] (s : ) (t : ) (x : α) :
insert x s \ insert x t = s \ insert x t
theorem Finset.sdiff_insert_of_not_mem {α : Type u_1} [inst : ] {s : } {x : α} (h : ¬x s) (t : ) :
s \ insert x t = s \ t
@[simp]
theorem Finset.sdiff_subset {α : Type u_1} [inst : ] (s : ) (t : ) :
s \ t s
theorem Finset.sdiff_ssubset {α : Type u_1} [inst : ] {s : } {t : } (h : t s) (ht : ) :
s \ t s
theorem Finset.union_sdiff_distrib {α : Type u_1} [inst : ] (s₁ : ) (s₂ : ) (t : ) :
(s₁ s₂) \ t = s₁ \ t s₂ \ t
theorem Finset.sdiff_union_distrib {α : Type u_1} [inst : ] (s : ) (t₁ : ) (t₂ : ) :
s \ (t₁ t₂) = s \ t₁ (s \ t₂)
theorem Finset.union_sdiff_self {α : Type u_1} [inst : ] (s : ) (t : ) :
(s t) \ t = s \ t
theorem Finset.sdiff_singleton_eq_erase {α : Type u_1} [inst : ] (a : α) (s : ) :
s \ {a} =
@[simp]
theorem Finset.sdiff_singleton_not_mem_eq_self {α : Type u_1} [inst : ] (s : ) {a : α} (ha : ¬a s) :
s \ {a} = s
theorem Finset.sdiff_sdiff_left' {α : Type u_1} [inst : ] (s : ) (t : ) (u : ) :
(s \ t) \ u = s \ t (s \ u)
theorem Finset.sdiff_insert {α : Type u_1} [inst : ] (s : ) (t : ) (x : α) :
s \ insert x t = Finset.erase (s \ t) x
theorem Finset.sdiff_insert_insert_of_mem_of_not_mem {α : Type u_1} [inst : ] {s : } {t : } {x : α} (hxs : x s) (hxt : ¬x t) :
insert x (s \ insert x t) = s \ t
theorem Finset.sdiff_erase {α : Type u_1} [inst : ] {s : } {x : α} (hx : x s) :
s \ = {x}
theorem Finset.sdiff_sdiff_self_left {α : Type u_1} [inst : ] (s : ) (t : ) :
s \ (s \ t) = s t
theorem Finset.sdiff_sdiff_eq_self {α : Type u_1} [inst : ] {s : } {t : } (h : t s) :
s \ (s \ t) = t
theorem Finset.sdiff_eq_sdiff_iff_inter_eq_inter {α : Type u_1} [inst : ] {s : } {t₁ : } {t₂ : } :
s \ t₁ = s \ t₂ s t₁ = s t₂
theorem Finset.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} [inst : ] (s : ) (t : ) :
s t = s \ t t \ s s t
theorem Finset.erase_eq_empty_iff {α : Type u_1} [inst : ] (s : ) (a : α) :
= s = s = {a}
theorem Finset.sdiff_disjoint {α : Type u_1} [inst : ] {s : } {t : } :
Disjoint (t \ s) s
theorem Finset.disjoint_sdiff {α : Type u_1} [inst : ] {s : } {t : } :
Disjoint s (t \ s)
theorem Finset.disjoint_sdiff_inter {α : Type u_1} [inst : ] (s : ) (t : ) :
Disjoint (s \ t) (s t)
theorem Finset.sdiff_eq_self_iff_disjoint {α : Type u_1} [inst : ] {s : } {t : } :
s \ t = s Disjoint s t
theorem Finset.sdiff_eq_self_of_disjoint {α : Type u_1} [inst : ] {s : } {t : } (h : Disjoint s t) :
s \ t = s

### Symmetric difference #

theorem Finset.mem_symmDiff {α : Type u_1} [inst : ] {s : } {t : } {a : α} :
a s t a s ¬a t a t ¬a s
@[simp]
theorem Finset.coe_symmDiff {α : Type u_1} [inst : ] {s : } {t : } :
↑(s t) = s t

### attach #

def Finset.attach {α : Type u_1} (s : ) :
Finset { x // x s }

attach s takes the elements of s and forms a new set of elements of the subtype {x // x ∈ s}∈ s}.

Equations
theorem Finset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [inst : ] {x : α} {s : } (hx : x s) :
<
@[simp]
theorem Finset.attach_val {α : Type u_1} (s : ) :
().val = Multiset.attach s.val
@[simp]
theorem Finset.mem_attach {α : Type u_1} (s : ) (x : { x // x s }) :
@[simp]
theorem Finset.attach_empty {α : Type u_1} :
@[simp]
theorem Finset.attach_nonempty_iff {α : Type u_1} (s : ) :
@[simp]
theorem Finset.attach_eq_empty_iff {α : Type u_1} (s : ) :
s =

### piecewise #

def Finset.piecewise {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] (i : α) :
δ i

s.piecewise f g is the function equal to f on the finset s, and to g on its complement.

Equations
theorem Finset.piecewise_insert_self {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : ] {j : α} [inst : (i : α) → Decidable (i insert j s)] :
Finset.piecewise (insert j s) f g j = f j
@[simp]
theorem Finset.piecewise_empty {α : Type u_1} {δ : αSort u_2} (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (i : α) → Decidable (i )] :
= g
theorem Finset.piecewise_coe {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] [inst : (j : α) → Decidable (j s)] :
Set.piecewise (s) f g =
@[simp]
theorem Finset.piecewise_eq_of_mem {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] {i : α} (hi : i s) :
Finset.piecewise s f g i = f i
@[simp]
theorem Finset.piecewise_eq_of_not_mem {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] {i : α} (hi : ¬i s) :
Finset.piecewise s f g i = g i
theorem Finset.piecewise_congr {α : Type u_1} {δ : αSort u_2} (s : ) [inst : (j : α) → Decidable (j s)] {f : (i : α) → δ i} {f' : (i : α) → δ i} {g : (i : α) → δ i} {g' : (i : α) → δ i} (hf : ∀ (i : α), i sf i = f' i) (hg : ∀ (i : α), ¬i sg i = g' i) :
@[simp]
theorem Finset.piecewise_insert_of_ne {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] [inst : ] {i : α} {j : α} [inst : (i : α) → Decidable (i insert j s)] (h : i j) :
theorem Finset.piecewise_insert {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] [inst : ] (j : α) [inst : (i : α) → Decidable (i insert j s)] :
theorem Finset.piecewise_cases {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] {i : α} (p : δ iProp) (hf : p (f i)) (hg : p (g i)) :
p (Finset.piecewise s f g i)
theorem Finset.piecewise_mem_set_pi {α : Type u_2} (s : ) [inst : (j : α) → Decidable (j s)] {δ : αType u_1} {t : Set α} {t' : (i : α) → Set (δ i)} {f : (i : α) → δ i} {g : (i : α) → δ i} (hf : f Set.pi t t') (hg : g Set.pi t t') :
Set.pi t t'
theorem Finset.piecewise_singleton {α : Type u_1} {δ : αSort u_2} (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : ] (i : α) :
theorem Finset.piecewise_piecewise_of_subset_left {α : Type u_1} {δ : αSort u_2} {s : } {t : } [inst : (i : α) → Decidable (i s)] [inst : (i : α) → Decidable (i t)] (h : s t) (f₁ : (a : α) → δ a) (f₂ : (a : α) → δ a) (g : (a : α) → δ a) :
@[simp]
theorem Finset.piecewise_idem_left {α : Type u_1} {δ : αSort u_2} (s : ) [inst : (j : α) → Decidable (j s)] (f₁ : (a : α) → δ a) (f₂ : (a : α) → δ a) (g : (a : α) → δ a) :
theorem Finset.piecewise_piecewise_of_subset_right {α : Type u_1} {δ : αSort u_2} {s : } {t : } [inst : (i : α) → Decidable (i s)] [inst : (i : α) → Decidable (i t)] (h : t s) (f : (a : α) → δ a) (g₁ : (a : α) → δ a) (g₂ : (a : α) → δ a) :
@[simp]
theorem Finset.piecewise_idem_right {α : Type u_1} {δ : αSort u_2} (s : ) [inst : (j : α) → Decidable (j s)] (f : (a : α) → δ a) (g₁ : (a : α) → δ a) (g₂ : (a : α) → δ a) :
theorem Finset.update_eq_piecewise {α : Type u_2} {β : Type u_1} [inst : ] (f : αβ) (i : α) (v : β) :
= Finset.piecewise {i} (fun x => v) f
theorem Finset.update_piecewise {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] [inst : ] (i : α) (v : δ i) :
theorem Finset.update_piecewise_of_mem {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] [inst : ] {i : α} (hi : i s) (v : δ i) :
theorem Finset.update_piecewise_of_not_mem {α : Type u_1} {δ : αSort u_2} (s : ) (f : (i : α) → δ i) (g : (i : α) → δ i) [inst : (j : α) → Decidable (j s)] [inst : ] {i : α} (hi : ¬