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

Lean refers to these operations as big operators. More information can be found in Mathlib/Algebra/BigOperators/Group/Finset.lean.

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

Finset.card, the size of a finset is defined in Mathlib/Data/Finset/Card.lean. 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 α).
• Finset.instCoeTCFinsetSet: Provides a coercion s : Finset α to s : Set α.
• Finset.instCoeSortFinsetType: 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

• 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}; 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, 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.lean. For the lattice structure on finsets, ⊥ is called bot with ⊥ = ∅ and ⊤ is called top with ⊤ = univ.

• Finset.instHasSubsetFinset: Lots of API about lattices, otherwise behaves as one would expect.
• Finset.instUnionFinset: Defines s ∪ t (or s ⊔ t) as the union of s and t. See Finset.sup/Finset.biUnion for finite unions.
• Finset.instInterFinset: Defines s ∩ t (or s ⊓ t) as the intersection of s and t. See Finset.inf for finite intersections.

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

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 ≠ ∅.

Equivalences between finsets

• The Mathlib/Logic/Equiv/Defs.lean 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.

• val : Multiset α

  The underlying multiset

• nodup : self.val.Nodup

  val contains no duplicates

theorem Finset.nodup {α : Type u_4} (self : Finset α) : self.val.Nodup

val contains no duplicates

instance Multiset.canLiftFinset {α : Type u_4} : CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup

Equations

• ⋯ = ⋯

theorem Finset.eq_of_veq {α : Type u_1} {s : Finset α} {t : Finset α} : s.val = t.val → s = t

theorem Finset.val_injective {α : Type u_1} : Function.Injective Finset.val

@[simp]

theorem Finset.val_inj {α : Type u_1} {s : Finset α} {t : Finset α} : s.val = t.val ↔ s = t

@[simp]

theorem Finset.dedup_eq_self {α : Type u_1} [DecidableEq α] (s : Finset α) : s.val.dedup = s.val

instance Finset.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Finset α)

Equations

• x✝.decidableEq x = decidable_of_iff (x✝.val = x.val) ⋯

membership

instance Finset.instMembership {α : Type u_1} : Membership α (Finset α)

Equations

• Finset.instMembership = { mem := fun (s : Finset α) (a : α) => a ∈ s.val }

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

instance Finset.decidableMem {α : Type u_1} [_h : DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ s)

Equations

• Finset.decidableMem a s = Multiset.decidableMem a s.val

@[simp]

theorem Finset.forall_mem_not_eq {α : Type u_1} {s : Finset α} {a : α} : (∀ b ∈ s, ¬a = b) ↔ a ∉ s

@[simp]

theorem Finset.forall_mem_not_eq' {α : Type u_1} {s : Finset α} {a : α} : (∀ b ∈ s, ¬b = a) ↔ a ∉ s

set coercion

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

Convert a finset to a set in the natural way.

Equations

• ↑s = {a : α | a ∈ s}

instance Finset.instCoeTCSet {α : Type u_1} : CoeTC (Finset α) (Set α)

Convert a finset to a set in the natural way.

Equations

• Finset.instCoeTCSet = { coe := Finset.toSet }

@[simp]

theorem Finset.mem_coe {α : Type u_1} {a : α} {s : Finset α} : a ∈ ↑s ↔ a ∈ s

@[simp]

theorem Finset.setOf_mem {α : Type u_4} {s : Finset α} : {a : α | a ∈ s} = ↑s

@[simp]

theorem Finset.coe_mem {α : Type u_1} {s : Finset α} (x : ↑↑s) : ↑x ∈ s

theorem Finset.mk_coe {α : Type u_1} {s : Finset α} (x : ↑↑s) {h : ↑x ∈ ↑s} : ⟨↑x, h⟩ = x

instance Finset.decidableMem' {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ ↑s)

Equations

• Finset.decidableMem' a s = Finset.decidableMem a s

extensionality

theorem Finset.ext_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂

theorem Finset.ext {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (h : ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) : s₁ = s₂

@[simp]

theorem Finset.coe_inj {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : ↑s₁ = ↑s₂ ↔ s₁ = s₂

theorem Finset.coe_injective {α : Type u_4} : Function.Injective Finset.toSet

type coercion

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

Coercion from a finset to the corresponding subtype.

Equations

• Finset.instCoeSortType = { coe := fun (s : Finset α) => { x : α // x ∈ s } }

theorem Finset.forall_coe {α : Type u_4} (s : Finset α) (p : { x : α // x ∈ s } → Prop) : (∀ (x : { x : α // x ∈ s }), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩

theorem Finset.exists_coe {α : Type u_4} (s : Finset α) (p : { x : α // x ∈ s } → Prop) : (∃ (x : { x : α // x ∈ s }), p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩

instance Finset.PiFinsetCoe.canLift (ι : Type u_4) (α : ι → Type u_5) [_ne : ∀ (i : ι), Nonempty (α i)] (s : Finset ι) : CanLift ((i : { x : ι // x ∈ s }) → α ↑i) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : { x : ι // x ∈ s }) => f ↑i) fun (x : (i : { x : ι // x ∈ s }) → α ↑i) => True

Equations

• ⋯ = ⋯

instance Finset.PiFinsetCoe.canLift' (ι : Type u_4) (α : Type u_5) [_ne : Nonempty α] (s : Finset ι) : CanLift ({ x : ι // x ∈ s } → α) (ι → α) (fun (f : ι → α) (i : { x : ι // x ∈ s }) => f ↑i) fun (x : { x : ι // x ∈ s } → α) => True

Equations

• ⋯ = ⋯

instance Finset.FinsetCoe.canLift {α : Type u_1} (s : Finset α) : CanLift α { x : α // x ∈ s } Subtype.val fun (a : α) => a ∈ s

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.coe_sort_coe {α : Type u_1} (s : Finset α) : ↑↑s = { x : α // x ∈ s }

Subset and strict subset relations

instance Finset.instHasSubset {α : Type u_1} : HasSubset (Finset α)

Equations

• Finset.instHasSubset = { Subset := fun (s t : Finset α) => ∀ ⦃a : α⦄, a ∈ s → a ∈ t }

instance Finset.instHasSSubset {α : Type u_1} : HasSSubset (Finset α)

Equations

• Finset.instHasSSubset = { SSubset := fun (s t : Finset α) => s ⊆ t ∧ ¬t ⊆ s }

instance Finset.partialOrder {α : Type u_1} : PartialOrder (Finset α)

Equations

• Finset.partialOrder = PartialOrder.mk ⋯

instance Finset.instIsReflSubset {α : Type u_1} : IsRefl (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

• ⋯ = ⋯

instance Finset.instIsTransSubset {α : Type u_1} : IsTrans (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

• ⋯ = ⋯

instance Finset.instIsAntisymmSubset {α : Type u_1} : IsAntisymm (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

• ⋯ = ⋯

instance Finset.instIsIrreflSSubset {α : Type u_1} : IsIrrefl (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• ⋯ = ⋯

instance Finset.instIsTransSSubset {α : Type u_1} : IsTrans (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• ⋯ = ⋯

instance Finset.instIsAsymmSSubset {α : Type u_1} : IsAsymm (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• ⋯ = ⋯

instance Finset.instIsNonstrictStrictOrderSubsetSSubset {α : Type u_1} : IsNonstrictStrictOrder (Finset α) (fun (x1 x2 : Finset α) => x1 ⊆ x2) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• ⋯ = ⋯

theorem Finset.subset_def {α : Type u_1} {s : Finset α} {t : Finset α} : s ⊆ t ↔ s.val ⊆ t.val

theorem Finset.ssubset_def {α : Type u_1} {s : Finset α} {t : Finset α} : s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s

theorem Finset.Subset.refl {α : Type u_1} (s : Finset α) : s ⊆ s

theorem Finset.Subset.rfl {α : Type u_1} {s : Finset α} : s ⊆ s

theorem Finset.subset_of_eq {α : Type u_1} {s : Finset α} {t : Finset α} (h : s = t) : s ⊆ t

theorem Finset.Subset.trans {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃

theorem Finset.Superset.trans {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} : s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃

theorem Finset.mem_of_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂

theorem Finset.not_mem_mono {α : Type u_1} {s : Finset α} {t : Finset α} (h : s ⊆ t) {a : α} : a ∉ t → a ∉ s

theorem Finset.Subset.antisymm {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂

theorem Finset.subset_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂

@[simp]

theorem Finset.coe_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : ↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂

theorem Finset.GCongr.coe_subset_coe {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁ ⊆ s₂ → ↑s₁ ⊆ ↑s₂

Alias of the reverse direction of Finset.coe_subset.

@[simp]

theorem Finset.val_le_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂

theorem Finset.Subset.antisymm_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁

theorem Finset.not_subset {α : Type u_1} {s : Finset α} {t : Finset α} : ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t

@[simp]

theorem Finset.le_eq_subset {α : Type u_1} : (fun (x1 x2 : Finset α) => x1 ≤ x2) = fun (x1 x2 : Finset α) => x1 ⊆ x2

@[simp]

theorem Finset.lt_eq_subset {α : Type u_1} : (fun (x1 x2 : Finset α) => x1 < x2) = fun (x1 x2 : Finset α) => x1 ⊂ x2

theorem Finset.le_iff_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂

theorem Finset.lt_iff_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂

@[simp]

theorem Finset.coe_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂

@[simp]

theorem Finset.val_lt_iff {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁.val < s₂.val ↔ s₁ ⊂ s₂

theorem Finset.val_strictMono {α : Type u_1} : StrictMono Finset.val

theorem Finset.ssubset_iff_subset_ne {α : Type u_1} {s : Finset α} {t : Finset α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t

theorem Finset.ssubset_iff_of_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁

theorem Finset.ssubset_of_ssubset_of_subset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃

theorem Finset.ssubset_of_subset_of_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} {s₃ : Finset α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) : s₁ ⊂ s₃

theorem Finset.exists_of_ssubset {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} (h : s₁ ⊂ s₂) : ∃ x ∈ s₂, x ∉ s₁

instance Finset.isWellFounded_ssubset {α : Type u_1} : IsWellFounded (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• ⋯ = ⋯

instance Finset.wellFoundedLT {α : Type u_1} : WellFoundedLT (Finset α)

Equations

• ⋯ = ⋯

Order embedding from Finset α to Set α

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

Coercion to Set α as an OrderEmbedding.

Equations

• Finset.coeEmb = { toFun := Finset.toSet, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Finset.coe_coeEmb {α : Type u_1} : ⇑Finset.coeEmb = Finset.toSet

Nonempty

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

The property s.Nonempty expresses the fact that the finset s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Equations

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

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

Equations

• Finset.decidableNonempty = Quotient.recOnSubsingleton s.val fun (l : List α) => match l with | [] => isFalse ⋯ | a :: l => isTrue ⋯

@[simp]

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

theorem Finset.nonempty_coe_sort {α : Type u_1} {s : Finset α} : Nonempty { x : α // x ∈ s } ↔ s.Nonempty

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

Alias of the reverse direction of Finset.coe_nonempty.

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

Alias of the reverse direction of Finset.nonempty_coe_sort.

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

@[deprecated Finset.Nonempty.exists_mem]

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

Alias of Finset.Nonempty.exists_mem.

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

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

theorem Finset.Nonempty.to_subtype {α : Type u_1} {s : Finset α} : s.Nonempty → Nonempty { x : α // x ∈ s }

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

empty

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

The empty finset

Equations

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

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

Equations

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

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

Equations

• Finset.inhabitedFinset = { default := ∅ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

theorem Finset.eq_empty_of_forall_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 α} : s ⊆ ∅ ↔ s = ∅

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem Finset.isEmpty_coe_sort {α : Type u_1} {s : Finset α} : IsEmpty { x : α // x ∈ s } ↔ s = ∅

instance Finset.instIsEmpty {α : Type u_1} : IsEmpty { x : α // x ∈ ∅ }

Equations

• ⋯ = ⋯

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

A Finset for an empty type is empty.

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

Equations

• Finset.instOrderBot = OrderBot.mk ⋯

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of Finset.empty_ssubset.

singleton

instance Finset.instSingleton {α : Type u_1} : Singleton α (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 DecidableEq instance for α.

Equations

• Finset.instSingleton = { 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 : Finset α} : s.val = {a} ↔ s = {a}

theorem Finset.singleton_injective {α : Type u_1} : Function.Injective singleton

@[simp]

theorem Finset.singleton_inj {α : Type u_1} {a : α} {b : α} : {a} = {b} ↔ a = b

@[simp]

theorem Finset.singleton_nonempty {α : Type u_1} (a : α) : {a}.Nonempty

@[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 : Finset α} {a : α} : ↑s = {a} ↔ s = {a}

theorem Finset.coe_subset_singleton {α : Type u_1} {s : Finset α} {a : α} : ↑s ⊆ {a} ↔ s ⊆ {a}

theorem Finset.singleton_subset_coe {α : Type u_1} {s : Finset α} {a : α} : {a} ⊆ ↑s ↔ {a} ⊆ s

theorem Finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : Finset α} {a : α} : s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

theorem Finset.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : Finset α} {a : α} : s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

theorem Finset.nonempty_iff_eq_singleton_default {α : Type u_1} [Unique α] {s : Finset α} : s.Nonempty ↔ s = {default}

theorem Finset.Nonempty.eq_singleton_default {α : Type u_1} [Unique α] {s : Finset α} : s.Nonempty → s = {default}

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

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 ∈ 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 = ∅

@[reducible, inline]

abbrev Finset.Nontrivial {α : Type u_1} (s : Finset α) : Prop

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

Equations

• s.Nontrivial = (↑s).Nontrivial

@[simp]

theorem Finset.not_nontrivial_empty {α : Type u_1} : ¬∅.Nontrivial

@[simp]

theorem Finset.not_nontrivial_singleton {α : Type u_1} {a : α} : ¬{a}.Nontrivial

theorem Finset.Nontrivial.ne_singleton {α : Type u_1} {s : Finset α} {a : α} (hs : s.Nontrivial) : s ≠ {a}

theorem Finset.Nontrivial.exists_ne {α : Type u_1} {s : Finset α} (hs : s.Nontrivial) (a : α) : ∃ b ∈ s, b ≠ 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) : s.Nontrivial ↔ s ≠ {a}

theorem Finset.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u_1} {s : Finset α} : s.Nonempty → (∃ (a : α), s = {a}) ∨ s.Nontrivial

instance Finset.instNontrivial {α : Type u_1} [Nonempty α] : Nontrivial (Finset α)

Equations

• ⋯ = ⋯

instance Finset.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (Finset α)

Equations

• Finset.instUniqueOfIsEmpty = { default := ∅, uniq := ⋯ }

instance Finset.instUniqueSubtypeMemSingleton {α : Type u_1} (i : α) : Unique { x : α // x ∈ {i} }

Equations

• Finset.instUniqueSubtypeMemSingleton i = { default := ⟨i, ⋯⟩, uniq := ⋯ }

@[simp]

theorem Finset.default_singleton {α : Type u_1} (i : α) : ↑default = i

cons

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

cons a s h is the set {a} ∪ s containing a and the elements of s. It is the same as insert a s when it is defined, but unlike insert a s it does not require DecidableEq α, and the union is guaranteed to be disjoint.

Equations

• Finset.cons a s h = { val := a ::ₘ s.val, nodup := ⋯ }

@[simp]

theorem Finset.mem_cons {α : Type u_1} {s : Finset α} {a : α} {b : α} {h : a ∉ s} : b ∈ Finset.cons a s h ↔ b = a ∨ b ∈ s

theorem Finset.mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {s : Finset α} {hb : b ∉ s} (ha : a ∈ s) : a ∈ Finset.cons b s hb

theorem Finset.mem_cons_self {α : Type u_1} (a : α) (s : Finset α) {h : a ∉ s} : a ∈ Finset.cons a s h

@[simp]

theorem Finset.cons_val {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : (Finset.cons a s h).val = a ::ₘ s.val

theorem Finset.forall_mem_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) (p : α → Prop) : (∀ x ∈ Finset.cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x

theorem Finset.forall_of_forall_cons {α : Type u_1} {s : Finset α} {a : α} {p : α → Prop} {h : a ∉ s} (H : ∀ x ∈ Finset.cons a s h✝, p x) (x : α) (h : 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 } = Finset.cons a { val := s, nodup := ⋯ } ⋯

@[simp]

theorem Finset.cons_empty {α : Type u_1} (a : α) : Finset.cons a ∅ ⋯ = {a}

@[simp]

theorem Finset.cons_nonempty {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : (Finset.cons a s h).Nonempty

@[deprecated Finset.cons_nonempty]

theorem Finset.nonempty_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : (Finset.cons a s h).Nonempty

Alias of Finset.cons_nonempty.

@[simp]

theorem Finset.cons_ne_empty {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : Finset.cons a s h ≠ ∅

@[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} : ↑(Finset.cons a s h) = insert a ↑s

theorem Finset.subset_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : s ⊆ Finset.cons a s h

theorem Finset.ssubset_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : s ⊂ Finset.cons a s h

theorem Finset.cons_subset {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} {h : a ∉ s} : Finset.cons a s h ⊆ t ↔ a ∈ t ∧ s ⊆ t

@[simp]

theorem Finset.cons_subset_cons {α : Type u_1} {s : Finset α} {t : Finset α} {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 : Finset α} {t : Finset α} : s ⊂ t ↔ ∃ (a : α) (h : a ∉ s), Finset.cons a s h ⊆ t

disjoint

theorem Finset.disjoint_left {α : Type u_1} {s : Finset α} {t : Finset α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t

theorem Finset.disjoint_right {α : Type u_1} {s : Finset α} {t : Finset α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

theorem Finset.disjoint_iff_ne {α : Type u_1} {s : Finset α} {t : Finset α} : Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

@[simp]

theorem Finset.disjoint_val {α : Type u_1} {s : Finset α} {t : Finset α} : s.val.Disjoint t.val ↔ Disjoint s t

theorem Disjoint.forall_ne_finset {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} {b : α} (h : Disjoint s t) (ha : a ∈ s) (hb : b ∈ t) : a ≠ b

theorem Finset.not_disjoint_iff {α : Type u_1} {s : Finset α} {t : Finset α} : ¬Disjoint s t ↔ ∃ a ∈ s, a ∈ t

theorem Finset.disjoint_of_subset_left {α : Type u_1} {s : Finset α} {t : Finset α} {u : Finset α} (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t

theorem Finset.disjoint_of_subset_right {α : Type u_1} {s : Finset α} {t : Finset α} {u : Finset α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t

@[simp]

theorem Finset.disjoint_empty_left {α : Type u_1} (s : Finset α) : Disjoint ∅ s

@[simp]

theorem Finset.disjoint_empty_right {α : Type u_1} (s : Finset α) : Disjoint s ∅

@[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 : α} : Disjoint s {a} ↔ a ∉ s

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 α) : Disjoint s s ↔ s = ∅

@[simp]

theorem Finset.disjoint_coe {α : Type u_1} {s : Finset α} {t : Finset α} : Disjoint ↑s ↑t ↔ Disjoint s t

@[simp]

theorem Finset.pairwiseDisjoint_coe {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ι → Finset α} : (s.PairwiseDisjoint fun (i : ι) => ↑(f i)) ↔ s.PairwiseDisjoint f

disjoint union

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

disjUnion s t h is the set such that a ∈ disjUnion 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

• s.disjUnion t h = { val := s.val + t.val, nodup := ⋯ }

@[simp]

theorem Finset.mem_disjUnion {α : Type u_4} {s : Finset α} {t : Finset α} {h : Disjoint s t} {a : α} : a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem Finset.coe_disjUnion {α : Type u_1} {s : Finset α} {t : Finset α} (h : Disjoint s t) : ↑(s.disjUnion t h) = ↑s ∪ ↑t

theorem Finset.disjUnion_comm {α : Type u_1} (s : Finset α) (t : Finset α) (h : Disjoint s t) : s.disjUnion t h = t.disjUnion s ⋯

@[simp]

theorem Finset.empty_disjUnion {α : Type u_1} (t : Finset α) (h : optParam (Disjoint ∅ t) ⋯) : ∅.disjUnion t h = t

@[simp]

theorem Finset.disjUnion_empty {α : Type u_1} (s : Finset α) (h : optParam (Disjoint s ∅) ⋯) : s.disjUnion ∅ h = s

theorem Finset.singleton_disjUnion {α : Type u_1} (a : α) (t : Finset α) (h : Disjoint {a} t) : {a}.disjUnion t h = Finset.cons a t ⋯

theorem Finset.disjUnion_singleton {α : Type u_1} (s : Finset α) (a : α) (h : Disjoint s {a}) : s.disjUnion {a} h = Finset.cons a s ⋯

insert

instance Finset.instInsert {α : Type u_1} [DecidableEq α] : Insert α (Finset α)

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

Equations

• Finset.instInsert = { insert := fun (a : α) (s : Finset α) => { val := Multiset.ndinsert a s.val, nodup := ⋯ } }

theorem Finset.insert_def {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a s = { val := Multiset.ndinsert a s.val, nodup := ⋯ }

@[simp]

theorem Finset.insert_val {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).val = Multiset.ndinsert a s.val

theorem Finset.insert_val' {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).val = (a ::ₘ s.val).dedup

theorem Finset.insert_val_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).val = a ::ₘ s.val

@[simp]

theorem Finset.mem_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} : a ∈ insert b s ↔ a = b ∨ a ∈ s

theorem Finset.mem_insert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : a ∈ insert a s

theorem Finset.mem_insert_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (h : a ∈ s) : a ∈ insert b s

theorem Finset.mem_of_mem_insert_of_ne {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (h : b ∈ insert a s) : b ≠ a → b ∈ s

theorem Finset.eq_of_not_mem_of_mem_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (ha : b ∈ insert a s) (hb : b ∉ s) : b = a

@[simp]

theorem Finset.insert_empty {α : Type u_1} [DecidableEq α] {a : α} : insert a ∅ = {a}

A version of LawfulSingleton.insert_emptyc_eq that works with dsimp.

@[simp]

theorem Finset.cons_eq_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s) : Finset.cons a s h = insert a s

@[simp]

theorem Finset.coe_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : ↑(insert a s) = insert a ↑s

theorem Finset.mem_insert_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} {y : α} : x ∈ insert y s ↔ x ∈ insert y ↑s

instance Finset.instLawfulSingleton {α : Type u_1} [DecidableEq α] : LawfulSingleton α (Finset α)

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.insert_eq_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∈ s) : insert a s = s

@[simp]

theorem Finset.insert_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} : insert a s = s ↔ a ∈ s

theorem Finset.insert_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} : insert a s ≠ s ↔ a ∉ s

theorem Finset.pair_eq_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a, a} = {a}

theorem Finset.Insert.comm {α : Type u_1} [DecidableEq α] (a : α) (b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s)

theorem Finset.coe_pair {α : Type u_1} [DecidableEq α] {a : α} {b : α} : ↑{a, b} = {a, b}

@[simp]

theorem Finset.coe_eq_pair {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} : ↑s = {a, b} ↔ s = {a, b}

theorem Finset.pair_comm {α : Type u_1} [DecidableEq α] (a : α) (b : α) : {a, b} = {b, a}

theorem Finset.insert_idem {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a (insert a s) = insert a s

@[simp]

theorem Finset.insert_nonempty {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).Nonempty

@[simp]

theorem Finset.insert_ne_empty {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a s ≠ ∅

instance Finset.instNonemptyElemToSetInsert {α : Type u_1} [DecidableEq α] (i : α) (s : Finset α) : Nonempty ↑↑(insert i s)

Equations

• ⋯ = ⋯

theorem Finset.ne_insert_of_not_mem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t

theorem Finset.insert_subset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

theorem Finset.insert_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t

@[simp]

theorem Finset.subset_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s ⊆ insert a s

theorem Finset.insert_subset_insert {α : Type u_1} [DecidableEq α] (a : α) {s : Finset α} {t : Finset α} (h : s ⊆ t) : insert a s ⊆ insert a t

@[simp]

theorem Finset.insert_subset_insert_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t

theorem Finset.insert_inj {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (ha : a ∉ s) : insert a s = insert b s ↔ a = b

theorem Finset.insert_inj_on {α : Type u_1} [DecidableEq α] (s : Finset α) : Set.InjOn (fun (a : α) => insert a s) (↑s)ᶜ

theorem Finset.ssubset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t

theorem Finset.ssubset_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∉ s) : s ⊂ insert a s

theorem Finset.cons_induction {α : Type u_4} {p : Finset α → Prop} (empty : p ∅) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)) (s : Finset α) : p s

theorem Finset.cons_induction_on {α : Type u_4} {p : Finset α → Prop} (s : Finset α) (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (Finset.cons a s h)) : p s

theorem Finset.induction {α : Type u_4} {p : Finset α → Prop} [DecidableEq α] (empty : p ∅) (insert : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (Insert.insert a s)) (s : Finset α) : p s

theorem Finset.induction_on {α : Type u_4} {p : Finset α → Prop} [DecidableEq α] (s : Finset α) (empty : p ∅) (insert : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (Insert.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_4} {p : Finset α → Prop} [DecidableEq α] (S : Finset α) (h₁ : p ∅) (h₂ : ∀ {a : α} {s : Finset α}, a ∈ S → s ⊆ S → a ∉ s → p s → p (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, then it holds for the Finset obtained by inserting a new element of S.

theorem Finset.Nonempty.cons_induction {α : Type u_4} {p : (s : Finset α) → s.Nonempty → Prop} (singleton : ∀ (a : α), p {a} ⋯) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a 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.

theorem Finset.Nonempty.exists_cons_eq {α : Type u_4} {s : Finset α} (hs : s.Nonempty) : ∃ (t : Finset α) (a : α) (ha : a ∉ t), Finset.cons a t ha = s

def Finset.subtypeInsertEquivOption {α : Type u_1} [DecidableEq α] {t : Finset α} {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} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

@[simp]

theorem Finset.disjoint_insert_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t

Lattice structure

instance Finset.instUnion {α : Type u_1} [DecidableEq α] : Union (Finset α)

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

Equations

• Finset.instUnion = { union := fun (s t : Finset α) => { val := s.val.ndunion t.val, nodup := ⋯ } }

instance Finset.instInter {α : Type u_1} [DecidableEq α] : Inter (Finset α)

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

Equations

• Finset.instInter = { inter := fun (s t : Finset α) => { val := s.val.ndinter t.val, nodup := ⋯ } }

instance Finset.instLattice {α : Type u_1} [DecidableEq α] : Lattice (Finset α)

Equations

• Finset.instLattice = Lattice.mk ⋯ ⋯ ⋯

@[simp]

theorem Finset.sup_eq_union {α : Type u_1} [DecidableEq α] : Sup.sup = Union.union

@[simp]

theorem Finset.inf_eq_inter {α : Type u_1} [DecidableEq α] : Inf.inf = Inter.inter

theorem Finset.disjoint_iff_inter_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : Disjoint s t ↔ s ∩ t = ∅

instance Finset.decidableDisjoint {α : Type u_1} [DecidableEq α] (U : Finset α) (V : Finset α) : Decidable (Disjoint U V)

Equations

• U.decidableDisjoint V = decidable_of_iff (∀ ⦃a : α⦄, a ∈ U → a ∉ V) ⋯

union

theorem Finset.union_val_nd {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t).val = s.val.ndunion t.val

@[simp]

theorem Finset.union_val {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t).val = s.val ∪ t.val

@[simp]

theorem Finset.mem_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem Finset.disjUnion_eq_union {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (h : Disjoint s t) : s.disjUnion t h = s ∪ t

theorem Finset.mem_union_left {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (t : Finset α) (h : a ∈ s) : a ∈ s ∪ t

theorem Finset.mem_union_right {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (s : Finset α) (h : a ∈ t) : a ∈ s ∪ t

theorem Finset.forall_mem_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {p : α → Prop} : (∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a

theorem Finset.not_mem_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t

@[simp]

theorem Finset.coe_union {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : ↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂

theorem Finset.union_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (hs : s ⊆ u) : t ⊆ u → s ∪ t ⊆ u

theorem Finset.subset_union_left {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} : s₁ ⊆ s₁ ∪ s₂

theorem Finset.subset_union_right {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} : s₂ ⊆ s₁ ∪ s₂

theorem Finset.union_subset_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} {v : Finset α} (hsu : s ⊆ u) (htv : t ⊆ v) : s ∪ t ⊆ u ∪ v

theorem Finset.union_subset_union_left {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t

theorem Finset.union_subset_union_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂

theorem Finset.union_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁

instance Finset.instCommutativeUnion {α : Type u_1} [DecidableEq α] : Std.Commutative fun (x1 x2 : Finset α) => x1 ∪ x2

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.union_assoc {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

instance Finset.instAssociativeUnion {α : Type u_1} [DecidableEq α] : Std.Associative fun (x1 x2 : Finset α) => x1 ∪ x2

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.union_idempotent {α : Type u_1} [DecidableEq α] (s : Finset α) : s ∪ s = s

instance Finset.instIdempotentOpUnion {α : Type u_1} [DecidableEq α] : Std.IdempotentOp fun (x1 x2 : Finset α) => x1 ∪ x2

Equations

• ⋯ = ⋯

theorem Finset.union_subset_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : s ∪ t ⊆ u) : s ⊆ u

theorem Finset.union_subset_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : s ∪ t ⊆ u) : t ⊆ u

theorem Finset.union_left_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∪ (t ∪ u) = t ∪ (s ∪ u)

theorem Finset.union_right_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ t

theorem Finset.union_self {α : Type u_1} [DecidableEq α] (s : Finset α) : s ∪ s = s

@[simp]

theorem Finset.union_empty {α : Type u_1} [DecidableEq α] (s : Finset α) : s ∪ ∅ = s

@[simp]

theorem Finset.empty_union {α : Type u_1} [DecidableEq α] (s : Finset α) : ∅ ∪ s = s

theorem Finset.Nonempty.inl {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s.Nonempty) : (s ∪ t).Nonempty

theorem Finset.Nonempty.inr {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : t.Nonempty) : (s ∪ t).Nonempty

theorem Finset.insert_eq {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a s = {a} ∪ s

@[simp]

theorem Finset.insert_union {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : insert a s ∪ t = insert a (s ∪ t)

@[simp]

theorem Finset.union_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : s ∪ insert a t = insert a (s ∪ t)

theorem Finset.insert_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : insert a (s ∪ t) = insert a s ∪ insert a t

@[simp]

theorem Finset.union_eq_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∪ t = s ↔ t ⊆ s

@[simp]

theorem Finset.left_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s = s ∪ t ↔ t ⊆ s

@[simp]

theorem Finset.union_eq_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∪ t = t ↔ s ⊆ t

@[simp]

theorem Finset.right_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s = t ∪ s ↔ t ⊆ s

theorem Finset.union_congr_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u

theorem Finset.union_congr_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) : s ∪ u = t ∪ u

theorem Finset.union_eq_union_iff_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t

theorem Finset.union_eq_union_iff_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u

@[simp]

theorem Finset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Finset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

theorem Finset.induction_on_union {α : Type u_1} [DecidableEq α] (P : Finset α → Finset α → 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 : Finset α) (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 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].

inter

theorem Finset.inter_val_nd {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : (s₁ ∩ s₂).val = s₁.val.ndinter s₂.val

@[simp]

theorem Finset.inter_val {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : (s₁ ∩ s₂).val = s₁.val ∩ s₂.val

@[simp]

theorem Finset.mem_inter {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂

theorem Finset.mem_of_mem_inter_left {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) : a ∈ s₁

theorem Finset.mem_of_mem_inter_right {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} (h : a ∈ s₁ ∩ s₂) : a ∈ s₂

theorem Finset.mem_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s₁ : Finset α} {s₂ : Finset α} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂

theorem Finset.inter_subset_left {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} : s₁ ∩ s₂ ⊆ s₁

theorem Finset.inter_subset_right {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} : s₁ ∩ s₂ ⊆ s₂

theorem Finset.subset_inter {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {u : Finset α} : s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

@[simp]

theorem Finset.coe_inter {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : ↑(s₁ ∩ s₂) = ↑s₁ ∩ ↑s₂

@[simp]

theorem Finset.union_inter_cancel_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : (s ∪ t) ∩ s = s

@[simp]

theorem Finset.union_inter_cancel_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : (s ∪ t) ∩ t = t

theorem Finset.inter_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : s₁ ∩ s₂ = s₂ ∩ s₁

@[simp]

theorem Finset.inter_assoc {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

theorem Finset.inter_left_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

theorem Finset.inter_right_comm {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

@[simp]

theorem Finset.inter_self {α : Type u_1} [DecidableEq α] (s : Finset α) : s ∩ s = s

@[simp]

theorem Finset.inter_empty {α : Type u_1} [DecidableEq α] (s : Finset α) : s ∩ ∅ = ∅

@[simp]

theorem Finset.empty_inter {α : Type u_1} [DecidableEq α] (s : Finset α) : ∅ ∩ s = ∅

@[simp]

theorem Finset.inter_union_self {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s ∩ (t ∪ s) = s

@[simp]

theorem Finset.insert_inter_of_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {a : α} (h : a ∈ s₂) : insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)

@[simp]

theorem Finset.inter_insert_of_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {a : α} (h : a ∈ s₁) : s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

@[simp]

theorem Finset.insert_inter_of_not_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {a : α} (h : a ∉ s₂) : insert a s₁ ∩ s₂ = s₁ ∩ s₂

@[simp]

theorem Finset.inter_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} {a : α} (h : a ∉ s₁) : s₁ ∩ insert a s₂ = s₁ ∩ s₂

@[simp]

theorem Finset.singleton_inter_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : a ∈ s) : {a} ∩ s = {a}

@[simp]

theorem Finset.singleton_inter_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (H : a ∉ s) : {a} ∩ s = ∅

theorem Finset.singleton_inter {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : {a} ∩ s = if a ∈ s then {a} else ∅

@[simp]

theorem Finset.inter_singleton_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∈ s) : s ∩ {a} = {a}

@[simp]

theorem Finset.inter_singleton_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : s ∩ {a} = ∅

theorem Finset.inter_singleton {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : s ∩ {a} = if a ∈ s then {a} else ∅

theorem Finset.inter_subset_inter {α : Type u_1} [DecidableEq α] {x : Finset α} {y : Finset α} {s : Finset α} {t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ s ⊆ y ∩ t

theorem Finset.inter_subset_inter_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : t ⊆ u) : s ∩ t ⊆ s ∩ u

theorem Finset.inter_subset_inter_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : s ⊆ t) : s ∩ u ⊆ t ∩ u

theorem Finset.inter_subset_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∩ t ⊆ s ∪ t

instance Finset.instDistribLattice {α : Type u_1} [DecidableEq α] : DistribLattice (Finset α)

Equations

• Finset.instDistribLattice = DistribLattice.mk ⋯

@[simp]

theorem Finset.union_left_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s ∪ (s ∪ t) = s ∪ t

theorem Finset.union_right_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s ∪ t ∪ t = s ∪ t

@[simp]

theorem Finset.inter_left_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s ∩ (s ∩ t) = s ∩ t

theorem Finset.inter_right_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s ∩ t ∩ t = s ∩ t

theorem Finset.inter_union_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

theorem Finset.union_inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

theorem Finset.union_inter_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

theorem Finset.inter_union_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

@[deprecated Finset.inter_union_distrib_left]

theorem Finset.inter_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Alias of Finset.inter_union_distrib_left.

@[deprecated Finset.union_inter_distrib_right]

theorem Finset.inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Alias of Finset.union_inter_distrib_right.

@[deprecated Finset.union_inter_distrib_left]

theorem Finset.union_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

Alias of Finset.union_inter_distrib_left.

@[deprecated Finset.inter_union_distrib_right]

theorem Finset.union_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

Alias of Finset.inter_union_distrib_right.

theorem Finset.union_union_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

theorem Finset.union_union_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

theorem Finset.inter_inter_distrib_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

theorem Finset.inter_inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

theorem Finset.union_union_union_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

theorem Finset.inter_inter_inter_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) (v : Finset α) : s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

theorem Finset.union_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

theorem Finset.union_subset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

theorem Finset.subset_inter_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u

@[simp]

theorem Finset.inter_eq_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∩ t = s ↔ s ⊆ t

@[simp]

theorem Finset.inter_eq_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : t ∩ s = s ↔ s ⊆ t

theorem Finset.inter_congr_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) : s ∩ t = s ∩ u

theorem Finset.inter_congr_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t ∩ u

theorem Finset.inter_eq_inter_iff_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u

theorem Finset.inter_eq_inter_iff_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t

theorem Finset.ite_subset_union {α : Type u_1} [DecidableEq α] (s : Finset α) (s' : Finset α) (P : Prop) [Decidable P] : (if P then s else s') ⊆ s ∪ s'

theorem Finset.inter_subset_ite {α : Type u_1} [DecidableEq α] (s : Finset α) (s' : Finset α) (P : Prop) [Decidable P] : s ∩ s' ⊆ if P then s else s'

theorem Finset.not_disjoint_iff_nonempty_inter {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : ¬Disjoint s t ↔ (s ∩ t).Nonempty

theorem Finset.Nonempty.not_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : (s ∩ t).Nonempty → ¬Disjoint s t

Alias of the reverse direction of Finset.not_disjoint_iff_nonempty_inter.

theorem Finset.disjoint_or_nonempty_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : Disjoint s t ∨ (s ∩ t).Nonempty

instance Finset.isDirected_le {α : Type u_1} : IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance Finset.isDirected_subset {α : Type u_1} : IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

• ⋯ = ⋯

erase

def Finset.erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : Finset α

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

Equations

• s.erase a = { val := s.val.erase a, nodup := ⋯ }

@[simp]

theorem Finset.erase_val {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : (s.erase a).val = s.val.erase a

@[simp]

theorem Finset.mem_erase {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} : a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s

theorem Finset.not_mem_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : a ∉ s.erase a

@[simp]

theorem Finset.erase_empty {α : Type u_1} [DecidableEq α] (a : α) : ∅.erase a = ∅

theorem Finset.Nontrivial.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nontrivial) : (s.erase a).Nonempty

@[simp]

theorem Finset.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : (s.erase a).Nonempty ↔ s.Nontrivial

@[simp]

theorem Finset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a}.erase a = ∅

theorem Finset.ne_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} : b ∈ s.erase a → b ≠ a

theorem Finset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} : b ∈ s.erase a → b ∈ s

theorem Finset.mem_erase_of_ne_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} : a ≠ b → a ∈ s → a ∈ s.erase b

theorem Finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [DecidableEq α] {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 bea.

@[simp]

theorem Finset.erase_eq_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : s.erase a = s

@[simp]

theorem Finset.erase_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} : s.erase a = s ↔ a ∉ s

@[simp]

theorem Finset.erase_insert_eq_erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : (insert a s).erase a = s.erase a

theorem Finset.erase_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).erase a = s

theorem Finset.erase_insert_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} (h : a ≠ b) : (insert a s).erase b = insert a (s.erase b)

theorem Finset.erase_cons_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} (ha : a ∉ s) (hb : a ≠ b) : (Finset.cons a s ha).erase b = Finset.cons a (s.erase b) ⋯

@[simp]

theorem Finset.insert_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∈ s) : insert a (s.erase a) = s

theorem Finset.erase_eq_iff_eq_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (hs : a ∈ s) (ht : a ∉ t) : s.erase a = t ↔ s = insert a t

theorem Finset.insert_erase_invOn {α : Type u_1} [DecidableEq α] {a : α} : Set.InvOn (insert a) (fun (s : Finset α) => s.erase a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s}

theorem Finset.erase_subset_erase {α : Type u_1} [DecidableEq α] (a : α) {s : Finset α} {t : Finset α} (h : s ⊆ t) : s.erase a ⊆ t.erase a

theorem Finset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s.erase a ⊆ s

theorem Finset.subset_erase {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} {t : Finset α} : s ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s

@[simp]

theorem Finset.coe_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : ↑(s.erase a) = ↑s \ {a}

theorem Finset.erase_ssubset {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∈ s) : s.erase a ⊂ s

theorem Finset.ssubset_iff_exists_subset_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

theorem Finset.erase_ssubset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : s.erase a ⊂ insert a s

theorem Finset.erase_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} : s.erase a ≠ s ↔ a ∈ s

theorem Finset.erase_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∉ s) : (Finset.cons a s h).erase a = s

theorem Finset.erase_idem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : (s.erase a).erase a = s.erase a

theorem Finset.erase_right_comm {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Finset α} : (s.erase a).erase b = (s.erase b).erase a

theorem Finset.subset_insert_iff {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} {t : Finset α} : s ⊆ insert a t ↔ s.erase a ⊆ t

theorem Finset.erase_insert_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).erase a ⊆ s

theorem Finset.insert_erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s ⊆ insert a (s.erase a)

theorem Finset.subset_insert_iff_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t

theorem Finset.erase_subset_iff_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a ∈ t) : s.erase a ⊆ t ↔ s ⊆ t

theorem Finset.erase_inj {α : Type u_1} [DecidableEq α] {x : α} {y : α} (s : Finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y

theorem Finset.erase_injOn {α : Type u_1} [DecidableEq α] (s : Finset α) : Set.InjOn s.erase ↑s

theorem Finset.erase_injOn' {α : Type u_1} [DecidableEq α] (a : α) : Set.InjOn (fun (s : Finset α) => s.erase a) {s : Finset α | a ∈ s}

theorem Finset.Nontrivial.exists_cons_eq {α : Type u_1} {s : Finset α} (hs : s.Nontrivial) : ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), Finset.cons a (Finset.cons b t hb) ⋯ = s

sdiff

instance Finset.instSDiff {α : Type u_1} [DecidableEq α] : SDiff (Finset α)

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

Equations

• Finset.instSDiff = { sdiff := fun (s₁ s₂ : Finset α) => { val := s₁.val - s₂.val, nodup := ⋯ } }

@[simp]

theorem Finset.sdiff_val {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : (s₁ \ s₂).val = s₁.val - s₂.val

@[simp]

theorem Finset.mem_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∈ s \ t ↔ a ∈ s ∧ a ∉ t

@[simp]

theorem Finset.inter_sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : s₁ ∩ (s₂ \ s₁) = ∅

instance Finset.instGeneralizedBooleanAlgebra {α : Type u_1} [DecidableEq α] : GeneralizedBooleanAlgebra (Finset α)

Equations

• Finset.instGeneralizedBooleanAlgebra = GeneralizedBooleanAlgebra.mk ⋯ ⋯

theorem Finset.not_mem_sdiff_of_mem_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a ∈ t) : a ∉ s \ t

theorem Finset.not_mem_sdiff_of_not_mem_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a ∉ s) : a ∉ s \ t

theorem Finset.union_sdiff_of_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s ⊆ t) : s ∪ t \ s = t

theorem Finset.sdiff_union_of_subset {α : Type u_1} [DecidableEq α] {s₁ : Finset α} {s₂ : Finset α} (h : s₁ ⊆ s₂) : s₂ \ s₁ ∪ s₁ = s₂

theorem Finset.inter_sdiff_assoc {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : (s ∩ t) \ u = s ∩ (t \ u)

@[deprecated Finset.inter_sdiff_assoc]

theorem Finset.inter_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s ∩ (t \ u) = (s ∩ t) \ u

@[simp]

theorem Finset.sdiff_inter_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : s₂ \ s₁ ∩ s₁ = ∅

theorem Finset.sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) : s₁ \ s₁ = ∅

theorem Finset.sdiff_inter_distrib_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : s \ (t ∩ u) = s \ t ∪ s \ u

@[simp]

theorem Finset.sdiff_inter_self_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s \ (s ∩ t) = s \ t

@[simp]

theorem Finset.sdiff_inter_self_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s \ (t ∩ s) = s \ t

@[simp]

theorem Finset.sdiff_empty {α : Type u_1} [DecidableEq α] {s : Finset α} : s \ ∅ = s

theorem Finset.sdiff_subset_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} {v : Finset α} (hst : s ⊆ t) (hvu : v ⊆ u) : s \ u ⊆ t \ v

@[simp]

theorem Finset.coe_sdiff {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : ↑(s₁ \ s₂) = ↑s₁ \ ↑s₂

@[simp]

theorem Finset.union_sdiff_self_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∪ t \ s = s ∪ t

@[simp]

theorem Finset.sdiff_union_self_eq_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s \ t ∪ t = s ∪ t

theorem Finset.union_sdiff_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t) \ s = t \ s

theorem Finset.union_sdiff_right {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t) \ t = s \ t

theorem Finset.union_sdiff_cancel_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) : (s ∪ t) \ s = t

theorem Finset.union_sdiff_cancel_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) : (s ∪ t) \ t = s

theorem Finset.union_sdiff_symm {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s ∪ t \ s = t ∪ s \ t

theorem Finset.sdiff_union_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s \ t ∪ s ∩ t = s

theorem Finset.sdiff_idem {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : (s \ t) \ t = s \ t

theorem Finset.subset_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

@[simp]

theorem Finset.sdiff_eq_empty_iff_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s \ t = ∅ ↔ s ⊆ t

theorem Finset.sdiff_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : (s \ t).Nonempty ↔ ¬s ⊆ t

@[simp]

theorem Finset.empty_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) : ∅ \ s = ∅

theorem Finset.insert_sdiff_of_not_mem {α : Type u_1} [DecidableEq α] (s : Finset α) {t : Finset α} {x : α} (h : x ∉ t) : insert x s \ t = insert x (s \ t)

theorem Finset.insert_sdiff_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} (s : Finset α) {x : α} (h : x ∈ t) : insert x s \ t = s \ t

@[simp]

theorem Finset.insert_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∉ s) : insert a s \ s = {a}

@[simp]

theorem Finset.insert_sdiff_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (x : α) : insert x s \ insert x t = s \ insert x t

theorem Finset.insert_sdiff_insert' {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hab : a ≠ b) (ha : a ∉ s) : insert a s \ insert b s = {a}

theorem Finset.erase_sdiff_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = {b}

theorem Finset.cons_sdiff_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} (hab : a ≠ b) (ha : a ∉ s) (hb : b ∉ s) : Finset.cons a s ha \ Finset.cons b s hb = {a}

theorem Finset.sdiff_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} (h : x ∉ s) (t : Finset α) : s \ insert x t = s \ t

@[simp]

theorem Finset.sdiff_subset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s \ t ⊆ s

theorem Finset.sdiff_ssubset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : t ⊆ s) (ht : t.Nonempty) : s \ t ⊂ s

theorem Finset.union_sdiff_distrib {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (t : Finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t

theorem Finset.sdiff_union_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t₁ : Finset α) (t₂ : Finset α) : s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)

theorem Finset.union_sdiff_self {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : (s ∪ t) \ t = s \ t

theorem Finset.sdiff_singleton_eq_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s \ {a} = s.erase a

theorem Finset.erase_eq {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : s.erase a = s \ {a}

theorem Finset.disjoint_erase_comm {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

theorem Finset.disjoint_insert_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ t) : Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

theorem Finset.disjoint_erase_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ s) : Disjoint (insert a s) (t.erase a) ↔ Disjoint s t

theorem Finset.disjoint_of_erase_left {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ t) (hst : Disjoint (s.erase a) t) : Disjoint s t

theorem Finset.disjoint_of_erase_right {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ s) (hst : Disjoint s (t.erase a)) : Disjoint s t

theorem Finset.inter_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : s ∩ t.erase a = (s ∩ t).erase a

@[simp]

theorem Finset.erase_inter {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (t : Finset α) : s.erase a ∩ t = (s ∩ t).erase a

theorem Finset.erase_sdiff_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : s.erase a \ t = (s \ t).erase a

theorem Finset.insert_union_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : insert a s ∪ t = s ∪ insert a t

theorem Finset.erase_inter_comm {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : s.erase a ∩ t = s ∩ t.erase a

theorem Finset.erase_union_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : (s ∪ t).erase a = s.erase a ∪ t.erase a

theorem Finset.insert_inter_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : insert a (s ∩ t) = insert a s ∩ insert a t

theorem Finset.erase_sdiff_distrib {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (a : α) : (s \ t).erase a = s.erase a \ t.erase a

theorem Finset.erase_union_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (ha : a ∈ t) (s : Finset α) : s.erase a ∪ t = s ∪ t

theorem Finset.union_erase_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) (t : Finset α) : s ∪ t.erase a = s ∪ t

@[simp, deprecated Finset.erase_eq_of_not_mem]

theorem Finset.sdiff_singleton_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∉ s) : s \ {a} = s

theorem Finset.Nontrivial.sdiff_singleton_nonempty {α : Type u_1} [DecidableEq α] {c : α} {s : Finset α} (hS : s.Nontrivial) : (s \ {c}).Nonempty

theorem Finset.sdiff_sdiff_left' {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (u : Finset α) : (s \ t) \ u = s \ t ∩ (s \ u)

theorem Finset.sdiff_union_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u

theorem Finset.sdiff_union_erase_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {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} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u

theorem Finset.sdiff_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (x : α) : s \ insert x t = (s \ t).erase x

theorem Finset.sdiff_insert_insert_of_mem_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {x : α} (hxs : x ∈ s) (hxt : x ∉ t) : insert x (s \ insert x t) = s \ t

theorem Finset.sdiff_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} (h : a ∈ s) : s \ t.erase a = insert a (s \ t)

theorem Finset.sdiff_erase_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : s \ s.erase a = {a}

theorem Finset.sdiff_sdiff_self_left {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s \ (s \ t) = s ∩ t

theorem Finset.sdiff_sdiff_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : t ⊆ s) : s \ (s \ t) = t

theorem Finset.sdiff_eq_sdiff_iff_inter_eq_inter {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} : s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂

theorem Finset.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

theorem Finset.erase_eq_empty_iff {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

theorem Finset.sdiff_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : Disjoint (t \ s) s

theorem Finset.disjoint_sdiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : Disjoint s (t \ s)

theorem Finset.disjoint_sdiff_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : Disjoint (s \ t) (s ∩ t)

theorem Finset.sdiff_eq_self_iff_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s \ t = s ↔ Disjoint s t

@[deprecated Finset.sdiff_eq_self_iff_disjoint]

theorem Finset.sdiff_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : s \ t = s ↔ Disjoint s t

Alias of Finset.sdiff_eq_self_iff_disjoint.

theorem Finset.sdiff_eq_self_of_disjoint {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) : s \ t = s

Symmetric difference

theorem Finset.mem_symmDiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} : a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

@[simp]

theorem Finset.coe_symmDiff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : ↑(symmDiff s t) = symmDiff ↑s ↑t

@[simp]

theorem Finset.symmDiff_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : symmDiff s t = ∅ ↔ s = t

@[simp]

theorem Finset.symmDiff_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : (symmDiff s t).Nonempty ↔ s ≠ t

attach

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

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

Equations

• s.attach = { val := s.val.attach, nodup := ⋯ }

theorem Finset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Finset α} (hx : x ∈ s) : sizeOf x < sizeOf s

@[simp]

theorem Finset.attach_val {α : Type u_1} (s : Finset α) : s.attach.val = s.val.attach

@[simp]

theorem Finset.mem_attach {α : Type u_1} (s : Finset α) (x : { x : α // x ∈ s }) : x ∈ s.attach

@[simp]

theorem Finset.attach_empty {α : Type u_1} : ∅.attach = ∅

@[simp]

theorem Finset.attach_nonempty_iff {α : Type u_1} {s : Finset α} : s.attach.Nonempty ↔ s.Nonempty

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

Alias of the reverse direction of Finset.attach_nonempty_iff.

@[simp]

theorem Finset.attach_eq_empty_iff {α : Type u_1} {s : Finset α} : s.attach = ∅ ↔ s = ∅

instance Finset.decidableDforallFinset {α : Type u_1} {s : Finset α} {p : (a : α) → a ∈ s → Prop} [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] : Decidable (∀ (a : α) (h : a ∈ s), p a h)

Equations

• Finset.decidableDforallFinset = Multiset.decidableDforallMultiset

instance Finset.instDecidableRelSubset {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

• x✝.instDecidableRelSubset x = Finset.decidableDforallFinset

instance Finset.instDecidableRelSSubset {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• x✝.instDecidableRelSSubset x = instDecidableAnd

instance Finset.instDecidableLE {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Finset α) => x1 ≤ x2

Equations

• Finset.instDecidableLE = Finset.instDecidableRelSubset

instance Finset.instDecidableLT {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Finset α) => x1 < x2

Equations

• Finset.instDecidableLT = Finset.instDecidableRelSSubset

instance Finset.decidableDExistsFinset {α : Type u_1} {s : Finset α} {p : (a : α) → a ∈ s → Prop} [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] : Decidable (∃ (a : α) (h : a ∈ s), p a h)

Equations

• Finset.decidableDExistsFinset = Multiset.decidableDexistsMultiset

instance Finset.decidableExistsAndFinset {α : Type u_1} {s : Finset α} {p : α → Prop} [_hp : (a : α) → Decidable (p a)] : Decidable (∃ a ∈ s, p a)

Equations

• Finset.decidableExistsAndFinset = decidable_of_iff (∃ (a : α) (_ : a ∈ s), p a) ⋯

instance Finset.decidableExistsAndFinsetCoe {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] : Decidable (∃ a ∈ ↑s, p a)

Equations

• Finset.decidableExistsAndFinsetCoe = Finset.decidableExistsAndFinset

instance Finset.decidableEqPiFinset {α : Type u_1} {s : Finset α} {β : α → Type u_4} [_h : (a : α) → DecidableEq (β a)] : DecidableEq ((a : α) → a ∈ s → β a)

decidable equality for functions whose domain is bounded by finsets

Equations

• Finset.decidableEqPiFinset = Multiset.decidableEqPiMultiset

filter

def Finset.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset α

Finset.filter p s is the set of elements of s that satisfy p.

For example, one can use s.filter (· ∈ t) to get the intersection of s with t : Set α as a Finset α (when a DecidablePred (· ∈ t) instance is available).

Equations

• Finset.filter p s = { val := Multiset.filter p s.val, nodup := ⋯ }

def Mathlib.Meta.knownToBeFinsetNotSet (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Bool

Return true if expectedType? is some (Finset ?α), throws throwUnsupportedSyntax if it is some (Set ?α), and returns false otherwise.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.knownToBeFinsetNotSet none = pure false

def Mathlib.Meta.elabFinsetBuilderSep : Lean.Elab.Term.TermElab

Elaborate set builder notation for Finset.

{x ∈ s | p x} is elaborated as Finset.filter (fun x ↦ p x) s if either the expected type is Finset ?α or the expected type is not Set ?α and s has expected type Finset ?α.

See also

• Data.Set.Defs for the Set builder notation elaborator that this elaborator partly overrides.
• Data.Fintype.Basic for the Finset builder notation elaborator handling syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.
• Order.LocallyFinite.Basic for the Finset builder notation elaborator handling syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.

TODO: Write a delaborator

Equations

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

@[simp]

theorem Finset.filter_val {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : (Finset.filter p s).val = Multiset.filter p s.val

@[simp]

theorem Finset.filter_subset {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset.filter p s ⊆ s

@[simp]

theorem Finset.mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {a : α} : a ∈ Finset.filter p s ↔ a ∈ s ∧ p a

theorem Finset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (x : α) (h : x ∈ Finset.filter p s) : x ∈ s

theorem Finset.filter_ssubset {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : Finset.filter p s ⊂ s ↔ ∃ x ∈ s, ¬p x

theorem Finset.filter_filter {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] (s : Finset α) : Finset.filter q (Finset.filter p s) = Finset.filter (fun (a : α) => p a ∧ q a) s

theorem Finset.filter_comm {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] (s : Finset α) : Finset.filter q (Finset.filter p s) = Finset.filter p (Finset.filter q s)

theorem Finset.filter_congr_decidable {α : Type u_1} (s : Finset α) (p : α → Prop) (h : DecidablePred p) [DecidablePred p] : Finset.filter p s = Finset.filter p s

@[simp]

theorem Finset.filter_True {α : Type u_1} {h : DecidablePred fun (x : α) => True} (s : Finset α) : Finset.filter (fun (x : α) => True) s = s

@[simp]

theorem Finset.filter_False {α : Type u_1} {h : DecidablePred fun (x : α) => False} (s : Finset α) : Finset.filter (fun (x : α) => False) s = ∅

theorem Finset.filter_eq_self {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : Finset.filter p s = s ↔ ∀ x ∈ s, p x

theorem Finset.filter_eq_empty_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : Finset.filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

theorem Finset.filter_nonempty_iff {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : (Finset.filter p s).Nonempty ↔ ∃ a ∈ s, p a

theorem Finset.filter_true_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) : Finset.filter p s = s

If all elements of a Finset satisfy the predicate p, s.filter p is s.

theorem Finset.filter_false_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, ¬p x) : Finset.filter p s = ∅

If all elements of a Finset fail to satisfy the predicate p, s.filter p is ∅.

@[simp]

theorem Finset.filter_const {α : Type u_1} (p : Prop) [Decidable p] (s : Finset α) : Finset.filter (fun (_a : α) => p) s = if p then s else ∅

theorem Finset.filter_congr {α : Type u_1} {p : α → Prop} {q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Finset α} (H : ∀ x ∈ s, p x ↔ q x) : Finset.filter p s = Finset.filter q s

@[simp]

theorem Finset.filter_empty {α : Type u_1} (p : α → Prop) [DecidablePred p] : Finset.filter p ∅ = ∅

theorem Finset.filter_subset_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Finset α} {t : Finset α} (h : s ⊆ t) : Finset.filter p s ⊆ Finset.filter p t

theorem Finset.monotone_filter_left {α : Type u_1} (p : α → Prop) [DecidablePred p] : Monotone (Finset.filter p)

theorem Finset.monotone_filter_right {α : Type u_1} (s : Finset α) ⦃p : α → Prop⦄ ⦃q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : p ≤ q) : Finset.filter p s ⊆ Finset.filter q s

@[simp]

theorem Finset.coe_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : ↑(Finset.filter p s) = {x : α | x ∈ s ∧ p x}

theorem Finset.subset_coe_filter_of_subset_forall {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) {t : Set α} (h₁ : t ⊆ ↑s) (h₂ : ∀ x ∈ t, p x) : t ⊆ ↑(Finset.filter p s)

theorem Finset.filter_singleton {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) : Finset.filter p {a} = if p a then {a} else ∅

theorem Finset.filter_cons_of_pos {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (s : Finset α) (ha : a ∉ s) (hp : p a) : Finset.filter p (Finset.cons a s ha) = Finset.cons a (Finset.filter p s) ⋯

theorem Finset.filter_cons_of_neg {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (s : Finset α) (ha : a ∉ s) (hp : ¬p a) : Finset.filter p (Finset.cons a s ha) = Finset.filter p s

theorem Finset.disjoint_filter {α : Type u_1} {s : Finset α} {p : α → Prop} {q : α → Prop} [DecidablePred p] [DecidablePred q] : Disjoint (Finset.filter p s) (Finset.filter q s) ↔ ∀ x ∈ s, p x → ¬q x

theorem Finset.disjoint_filter_filter {α : Type u_1} {s : Finset α} {t : Finset α} {p : α → Prop} {q : α → Prop} [DecidablePred p] [DecidablePred q] : Disjoint s t → Disjoint (Finset.filter p s) (Finset.filter q t)

theorem Finset.disjoint_filter_filter' {α : Type u_1} (s : Finset α) (t : Finset α) {p : α → Prop} {q : α → Prop} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) : Disjoint (Finset.filter p s) (Finset.filter q t)

theorem Finset.disjoint_filter_filter_neg {α : Type u_1} (s : Finset α) (t : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)

@[deprecated Finset.disjoint_filter_filter_neg]

theorem Finset.filter_inter_filter_neg_eq {α : Type u_1} (s : Finset α) (t : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)

Alias of Finset.disjoint_filter_filter_neg.

theorem Finset.filter_disj_union {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) (t : Finset α) (h : Disjoint s t) : Finset.filter p (s.disjUnion t h) = (Finset.filter p s).disjUnion (Finset.filter p t) ⋯

theorem Set.pairwiseDisjoint_filter {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set β) (t : Finset α) : s.PairwiseDisjoint fun (x : β) => Finset.filter (fun (x_1 : α) => f x_1 = x) t

theorem Finset.filter_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] {a : α} (s : Finset α) (ha : a ∉ s) : Finset.filter p (Finset.cons a s ha) = if p a then Finset.cons a (Finset.filter p s) ⋯ else Finset.filter p s

theorem Finset.filter_union {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : Finset.filter p (s₁ ∪ s₂) = Finset.filter p s₁ ∪ Finset.filter p s₂

theorem Finset.filter_union_right {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) : Finset.filter p s ∪ Finset.filter q s = Finset.filter (fun (x : α) => p x ∨ q x) s

theorem Finset.filter_mem_eq_inter {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [(i : α) → Decidable (i ∈ t)] : Finset.filter (fun (i : α) => i ∈ t) s = s ∩ t

theorem Finset.filter_inter_distrib {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) : Finset.filter p (s ∩ t) = Finset.filter p s ∩ Finset.filter p t

theorem Finset.filter_inter {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) : Finset.filter p s ∩ t = Finset.filter p (s ∩ t)

theorem Finset.inter_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s : Finset α) (t : Finset α) : s ∩ Finset.filter p t = Finset.filter p (s ∩ t)

theorem Finset.filter_insert {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) : Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s

theorem Finset.filter_erase {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) : Finset.filter p (s.erase a) = (Finset.filter p s).erase a

theorem Finset.filter_or {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : α) => p a ∨ q a) s = Finset.filter p s ∪ Finset.filter q s

theorem Finset.filter_and {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : α) => p a ∧ q a) s = Finset.filter p s ∩ Finset.filter q s

theorem Finset.filter_not {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : α) => ¬p a) s = s \ Finset.filter p s

theorem Finset.filter_and_not {α : Type u_1} [DecidableEq α] (s : Finset α) (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] : Finset.filter (fun (a : α) => p a ∧ ¬q a) s = Finset.filter p s \ Finset.filter q s

theorem Finset.sdiff_eq_filter {α : Type u_1} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) : s₁ \ s₂ = Finset.filter (fun (x : α) => x ∉ s₂) s₁

theorem Finset.subset_union_elim {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ : Set α} {t₂ : Set α} (h : ↑s ⊆ t₁ ∪ t₂) : ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

theorem Finset.filter_eq {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (Eq b) s = if b ∈ s then {b} else ∅

After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to filter_eq' with the equality the other way.

theorem Finset.filter_eq' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (fun (a : β) => a = b) s = if b ∈ s then {b} else ∅

After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to filter_eq with the equality the other way.

theorem Finset.filter_ne {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (fun (a : β) => b ≠ a) s = s.erase b

theorem Finset.filter_ne' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (fun (a : β) => a ≠ b) s = s.erase b

theorem Finset.filter_union_filter_of_codisjoint {α : Type u_1} (p : α → Prop) (q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) (h : Codisjoint p q) : Finset.filter p s ∪ Finset.filter q s = s

theorem Finset.filter_union_filter_neg_eq {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] [(x : α) → Decidable ¬p x] (s : Finset α) : Finset.filter p s ∪ Finset.filter (fun (a : α) => ¬p a) s = s

theorem Finset.filter_inj {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {t : Finset α} : Finset.filter p s = Finset.filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)

theorem Finset.filter_inj' {α : Type u_1} {p : α → Prop} {q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Finset α} : Finset.filter p s = Finset.filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)

range

def Finset.range (n : ℕ) : Finset ℕ

range n is the set of natural numbers less than n.

Equations

• Finset.range n = { val := Multiset.range n, nodup := ⋯ }

@[simp]

theorem Finset.range_val (n : ℕ) : (Finset.range n).val = Multiset.range n

@[simp]

theorem Finset.mem_range {n : ℕ} {m : ℕ} : m ∈ Finset.range n ↔ m < n

@[simp]

theorem Finset.coe_range (n : ℕ) : ↑(Finset.range n) = Set.Iio n

@[simp]

theorem Finset.range_zero : Finset.range 0 = ∅

@[simp]

theorem Finset.range_one : Finset.range 1 = {0}

theorem Finset.range_succ {n : ℕ} : Finset.range n.succ = insert n (Finset.range n)

theorem Finset.range_add_one {n : ℕ} : Finset.range (n + 1) = insert n (Finset.range n)

theorem Finset.not_mem_range_self {n : ℕ} : n ∉ Finset.range n

theorem Finset.self_mem_range_succ (n : ℕ) : n ∈ Finset.range (n + 1)

@[simp]

theorem Finset.range_subset {n : ℕ} {m : ℕ} : Finset.range n ⊆ Finset.range m ↔ n ≤ m

theorem Finset.range_mono : Monotone Finset.range

theorem GCongr.finset_range_subset_of_le {n : ℕ} {m : ℕ} : n ≤ m → Finset.range n ⊆ Finset.range m

Alias of the reverse direction of Finset.range_subset.

theorem Finset.mem_range_succ_iff {a : ℕ} {b : ℕ} : a ∈ Finset.range b.succ ↔ a ≤ b

theorem Finset.mem_range_le {n : ℕ} {x : ℕ} (hx : x ∈ Finset.range n) : x ≤ n

theorem Finset.mem_range_sub_ne_zero {n : ℕ} {x : ℕ} (hx : x ∈ Finset.range n) : n - x ≠ 0

@[simp]

theorem Finset.nonempty_range_iff {n : ℕ} : (Finset.range n).Nonempty ↔ n ≠ 0

theorem Finset.Aesop.range_nonempty {n : ℕ} : n ≠ 0 → (Finset.range n).Nonempty

Alias of the reverse direction of Finset.nonempty_range_iff.

@[simp]

theorem Finset.range_eq_empty_iff {n : ℕ} : Finset.range n = ∅ ↔ n = 0

theorem Finset.nonempty_range_succ {n : ℕ} : (Finset.range (n + 1)).Nonempty

@[simp]

theorem Finset.range_filter_eq {n : ℕ} {m : ℕ} : Finset.filter (fun (x : ℕ) => x = m) (Finset.range n) = if m < n then {m} else ∅

theorem Finset.range_nontrivial {n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial

theorem Finset.exists_nat_subset_range (s : Finset ℕ) : ∃ (n : ℕ), s ⊆ Finset.range n

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

theorem Finset.exists_mem_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (p : α → Prop) : (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x

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

theorem Finset.forall_mem_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (p : α → Prop) : (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x

theorem Finset.forall_of_forall_insert {α : Type u_1} [DecidableEq α] {p : α → Prop} {a : α} {s : Finset α} (H : ∀ x ∈ insert a s, p x) (x : α) (h : x ∈ s) : p x

Useful in proofs by induction.

def notMemRangeEquiv (k : ℕ) : { n : ℕ // n ∉ Multiset.range k } ≃ ℕ

Equivalence between the set of natural numbers which are ≥ k and ℕ, given by n → n - k.

Equations

• notMemRangeEquiv k = { toFun := fun (i : { n : ℕ // n ∉ Multiset.range k }) => ↑i - k, invFun := fun (j : ℕ) => ⟨j + k, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem coe_notMemRangeEquiv (k : ℕ) : ⇑(notMemRangeEquiv k) = fun (i : { n : ℕ // n ∉ Multiset.range k }) => ↑i - k

@[simp]

theorem coe_notMemRangeEquiv_symm (k : ℕ) : ⇑(notMemRangeEquiv k).symm = fun (j : ℕ) => ⟨j + k, ⋯⟩

dedup on list and multiset

def Multiset.toFinset {α : Type u_1} [DecidableEq α] (s : Multiset α) : Finset α

toFinset s removes duplicates from the multiset s to produce a finset.

Equations

• s.toFinset = { val := s.dedup, nodup := ⋯ }

@[simp]

theorem Multiset.toFinset_val {α : Type u_1} [DecidableEq α] (s : Multiset α) : s.toFinset.val = s.dedup

theorem Multiset.toFinset_eq {α : Type u_1} [DecidableEq α] {s : Multiset α} (n : s.Nodup) : { val := s, nodup := n } = s.toFinset

theorem Multiset.Nodup.toFinset_inj {α : Type u_1} [DecidableEq α] {l : Multiset α} {l' : Multiset α} (hl : l.Nodup) (hl' : l'.Nodup) (h : l.toFinset = l'.toFinset) : l = l'

@[simp]

theorem Multiset.mem_toFinset {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s.toFinset ↔ a ∈ s

@[simp]

theorem Multiset.toFinset_zero {α : Type u_1} [DecidableEq α] : Multiset.toFinset 0 = ∅

@[simp]

theorem Multiset.toFinset_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : (a ::ₘ s).toFinset = insert a s.toFinset

@[simp]

theorem Multiset.toFinset_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a}.toFinset = {a}

@[simp]

theorem Multiset.toFinset_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : (s + t).toFinset = s.toFinset ∪ t.toFinset

@[simp]

theorem Multiset.toFinset_nsmul {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ℕ) : n ≠ 0 → (n • s).toFinset = s.toFinset

theorem Multiset.toFinset_eq_singleton_iff {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : s.toFinset = {a} ↔ Multiset.card s ≠ 0 ∧ s = Multiset.card s • {a}

@[simp]

theorem Multiset.toFinset_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

@[simp]

theorem Multiset.toFinset_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

@[simp]

theorem Multiset.toFinset_eq_empty {α : Type u_1} [DecidableEq α] {m : Multiset α} : m.toFinset = ∅ ↔ m = 0

@[simp]

theorem Multiset.toFinset_nonempty {α : Type u_1} [DecidableEq α] {s : Multiset α} : s.toFinset.Nonempty ↔ s ≠ 0

theorem Multiset.Aesop.toFinset_nonempty_of_ne {α : Type u_1} [DecidableEq α] {s : Multiset α} : s ≠ 0 → s.toFinset.Nonempty

Alias of the reverse direction of Multiset.toFinset_nonempty.

@[simp]

theorem Multiset.toFinset_subset {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} : s.toFinset ⊆ t.toFinset ↔ s ⊆ t

@[simp]

theorem Multiset.toFinset_ssubset {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} : s.toFinset ⊂ t.toFinset ↔ s ⊂ t

@[simp]

theorem Multiset.toFinset_dedup {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.dedup.toFinset = m.toFinset

@[simp]

theorem Multiset.toFinset_filter {α : Type u_1} [DecidableEq α] (s : Multiset α) (p : α → Prop) [DecidablePred p] : (Multiset.filter p s).toFinset = Finset.filter p s.toFinset

instance Multiset.isWellFounded_ssubset {β : Type u_2} : IsWellFounded (Multiset β) fun (x1 x2 : Multiset β) => x1 ⊂ x2

Equations

• ⋯ = ⋯

@[simp]

theorem Finset.val_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : s.val.toFinset = s

theorem Finset.val_le_iff_val_subset {α : Type u_1} {a : Finset α} {b : Multiset α} : a.val ≤ b ↔ a.val ⊆ b

def List.toFinset {α : Type u_1} [DecidableEq α] (l : List α) : Finset α

toFinset l removes duplicates from the list l to produce a finset.

Equations

• l.toFinset = (↑l).toFinset

@[simp]

theorem List.toFinset_val {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset.val = ↑l.dedup

@[simp]

theorem List.toFinset_coe {α : Type u_1} [DecidableEq α] (l : List α) : (↑l).toFinset = l.toFinset

theorem List.toFinset_eq {α : Type u_1} [DecidableEq α] {l : List α} (n : l.Nodup) : { val := ↑l, nodup := n } = l.toFinset

@[simp]

theorem List.mem_toFinset {α : Type u_1} [DecidableEq α] {l : List α} {a : α} : a ∈ l.toFinset ↔ a ∈ l

@[simp]

theorem List.coe_toFinset {α : Type u_1} [DecidableEq α] (l : List α) : ↑l.toFinset = {a : α | a ∈ l}

@[simp]

theorem List.toFinset_nil {α : Type u_1} [DecidableEq α] : [].toFinset = ∅

@[simp]

theorem List.toFinset_cons {α : Type u_1} [DecidableEq α] {l : List α} {a : α} : (a :: l).toFinset = insert a l.toFinset

theorem List.toFinset_surj_on {α : Type u_1} [DecidableEq α] : Set.SurjOn List.toFinset {l : List α | l.Nodup} Set.univ

theorem List.toFinset_surjective {α : Type u_1} [DecidableEq α] : Function.Surjective List.toFinset

theorem List.toFinset_eq_iff_perm_dedup {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} : l.toFinset = l'.toFinset ↔ l.dedup.Perm l'.dedup

theorem List.toFinset.ext_iff {α : Type u_1} [DecidableEq α] {a : List α} {b : List α} : a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

theorem List.toFinset.ext {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} : (∀ (x : α), x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset

theorem List.toFinset_eq_of_perm {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) (h : l.Perm l') : l.toFinset = l'.toFinset

theorem List.perm_of_nodup_nodup_toFinset_eq {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) (h : l.toFinset = l'.toFinset) : l.Perm l'

@[simp]

theorem List.toFinset_append {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} : (l ++ l').toFinset = l.toFinset ∪ l'.toFinset

@[simp]

theorem List.toFinset_reverse {α : Type u_1} [DecidableEq α] {l : List α} : l.reverse.toFinset = l.toFinset

theorem List.toFinset_replicate_of_ne_zero {α : Type u_1} [DecidableEq α] {a : α} {n : ℕ} (hn : n ≠ 0) : (List.replicate n a).toFinset = {a}

@[simp]

theorem List.toFinset_union {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) : (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

@[simp]

theorem List.toFinset_inter {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) : (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

@[simp]

theorem List.toFinset_eq_empty_iff {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset = ∅ ↔ l = []

@[simp]

theorem List.toFinset_nonempty_iff {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset.Nonempty ↔ l ≠ []

theorem List.Aesop.toFinset_nonempty_of_ne {α : Type u_1} [DecidableEq α] (l : List α) : l ≠ [] → l.toFinset.Nonempty

Alias of the reverse direction of List.toFinset_nonempty_iff.

@[simp]

theorem List.toFinset_filter {α : Type u_1} [DecidableEq α] (s : List α) (p : α → Bool) : (List.filter p s).toFinset = Finset.filter (fun (x : α) => p x = true) s.toFinset

noncomputable def Finset.toList {α : Type u_1} (s : Finset α) : List α

Produce a list of the elements in the finite set using choice.

Equations

• s.toList = s.val.toList

theorem Finset.nodup_toList {α : Type u_1} (s : Finset α) : s.toList.Nodup

@[simp]

theorem Finset.mem_toList {α : Type u_1} {a : α} {s : Finset α} : a ∈ s.toList ↔ a ∈ s

@[simp]

theorem Finset.toList_eq_nil {α : Type u_1} {s : Finset α} : s.toList = [] ↔ s = ∅

theorem Finset.empty_toList {α : Type u_1} {s : Finset α} : s.toList.isEmpty = true ↔ s = ∅

@[simp]

theorem Finset.toList_empty {α : Type u_1} : ∅.toList = []

theorem Finset.Nonempty.toList_ne_nil {α : Type u_1} {s : Finset α} (hs : s.Nonempty) : s.toList ≠ []

theorem Finset.Nonempty.not_empty_toList {α : Type u_1} {s : Finset α} (hs : s.Nonempty) : ¬s.toList.isEmpty = true

@[simp]

theorem Finset.coe_toList {α : Type u_1} (s : Finset α) : ↑s.toList = s.val

@[simp]

theorem Finset.toList_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : s.toList.toFinset = s

theorem List.toFinset_toList {α : Type u_1} [DecidableEq α] {s : List α} (hs : s.Nodup) : s.toFinset.toList.Perm s

@[simp]

theorem Finset.toList_eq_singleton_iff {α : Type u_1} {a : α} {s : Finset α} : s.toList = [a] ↔ s = {a}

@[simp]

theorem Finset.toList_singleton {α : Type u_1} (a : α) : {a}.toList = [a]

theorem Finset.exists_list_nodup_eq {α : Type u_1} [DecidableEq α] (s : Finset α) : ∃ (l : List α), l.Nodup ∧ l.toFinset = s

theorem Finset.toList_cons {α : Type u_1} {a : α} {s : Finset α} (h : a ∉ s) : (Finset.cons a s h).toList.Perm (a :: s.toList)

theorem Finset.toList_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).toList.Perm (a :: s.toList)

choose

def Finset.chooseX {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : { a : α // a ∈ l ∧ p a }

Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the corresponding subtype.

Equations

• Finset.chooseX p l hp = Multiset.chooseX p l.val hp

def Finset.choose {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : α

Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the ambient type.

Equations

• Finset.choose p l hp = ↑(Finset.chooseX p l hp)

theorem Finset.choose_spec {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : Finset.choose p l hp ∈ l ∧ p (Finset.choose p l hp)

theorem Finset.choose_mem {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : Finset.choose p l hp ∈ l

theorem Finset.choose_property {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : p (Finset.choose p l hp)

theorem Finset.pairwise_subtype_iff_pairwise_finset' {α : Type u_1} {β : Type u_2} {s : Finset α} (r : β → β → Prop) (f : α → β) : Pairwise (r on fun (x : { x : α // x ∈ s }) => f ↑x) ↔ (↑s).Pairwise (r on f)

theorem Finset.pairwise_subtype_iff_pairwise_finset {α : Type u_1} {s : Finset α} (r : α → α → Prop) : Pairwise (r on fun (x : { x : α // x ∈ s }) => ↑x) ↔ (↑s).Pairwise r

theorem Finset.pairwise_cons' {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) : Pairwise (r on fun (a_1 : { x : α // x ∈ Finset.cons a s ha }) => f ↑a_1) ↔ Pairwise (r on fun (a : { x : α // x ∈ s }) => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

theorem Finset.pairwise_cons {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (r : α → α → Prop) : Pairwise (r on fun (a_1 : { x : α // x ∈ Finset.cons a s ha }) => ↑a_1) ↔ Pairwise (r on fun (a : { x : α // x ∈ s }) => ↑a) ∧ ∀ b ∈ s, r a b ∧ r b a

def Equiv.Finset.union {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (h : Disjoint s t) : { x : α // x ∈ s } ⊕ { x : α // x ∈ t } ≃ { x : α // x ∈ s ∪ t }

The disjoint union of finsets is a sum

Equations

• Equiv.Finset.union s t h = ((Equiv.Set.ofEq ⋯).trans (Equiv.Set.union ⋯)).symm

@[simp]

theorem Equiv.Finset.union_symm_inl {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) (x : { x : α // x ∈ s }) : (Equiv.Finset.union s t h) (Sum.inl x) = ⟨↑x, ⋯⟩

@[simp]

theorem Equiv.Finset.union_symm_inr {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) (y : { x : α // x ∈ t }) : (Equiv.Finset.union s t h) (Sum.inr y) = ⟨↑y, ⋯⟩

def Equiv.piFinsetUnion {ι : Type u_5} [DecidableEq ι] (α : ι → Type u_4) {s : Finset ι} {t : Finset ι} (h : Disjoint s t) : ((i : { x : ι // x ∈ s }) → α ↑i) × ((i : { x : ι // x ∈ t }) → α ↑i) ≃ ((i : { x : ι // x ∈ s ∪ t }) → α ↑i)

The type of dependent functions on the disjoint union of finsets s ∪ t is equivalent to the type of pairs of functions on s and on t. This is similar to Equiv.sumPiEquivProdPi.

Equations

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

theorem Multiset.disjoint_toFinset {α : Type u_1} [DecidableEq α] {m1 : Multiset α} {m2 : Multiset α} : Disjoint m1.toFinset m2.toFinset ↔ m1.Disjoint m2

theorem List.disjoint_toFinset_iff_disjoint {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} : Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l'

def Mathlib.Meta.proveFinsetNonempty {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) : Lean.MetaM (Option Q(«$s».Nonempty))

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

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

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

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

Equations

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