mathlib3 documentation

data.finset.basic

Finite sets #

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

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

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

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

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

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

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

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

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

Main declarations #

Main definitions #

Finset constructions #

Finsets from functions #

The lattice structure on subsets of finsets #

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

Operations on two or more finsets #

Maps constructed using finsets #

Predicates on finsets #

Equivalences between finsets #

Tags #

finite sets, finset

source
structure finset (α : Type u_4) :
Type u_4

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

Instances for finset
source
@[protected, instance]
def multiset.can_lift_finset {α : Type u_1} :
can_lift (multiset α) (finset α) finset.val multiset.nodup
Equations
source
theorem finset.eq_of_veq {α : Type u_1} {s t : finset α} :
s.val = t.val → s = t
source
theorem finset.val_injective {α : Type u_1} :
function.injective finset.val
source
@[simp]
theorem finset.val_inj {α : Type u_1} {s t : finset α} :
s.val = t.val ↔ s = t
source
@[simp]
theorem finset.dedup_eq_self {α : Type u_1} [decidable_eq α] (s : finset α) :
s.val.dedup = s.val
source
@[protected, instance]
def finset.has_decidable_eq {α : Type u_1} [decidable_eq α] :
decidable_eq (finset α)
Equations

membership #

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

set coercion #

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

Convert a finset to a set in the natural way.

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

extensionality #

source
theorem finset.ext_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂
source
@[ext]
theorem finset.ext {α : Type u_1} {s₁ s₂ : finset α} :
(∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂
source
@[simp, norm_cast]
theorem finset.coe_inj {α : Type u_1} {s₁ s₂ : finset α} :
↑s₁ = ↑s₂ ↔ s₁ = s₂
source
theorem finset.coe_injective {α : Type u_1} :
function.injective coe

type coercion #

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

Coercion from a finset to the corresponding subtype.

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

Subset and strict subset relations #

source
@[protected, instance]
def finset.has_subset {α : Type u_1} :
has_subset (finset α)
Equations
source
@[protected, instance]
def finset.has_ssubset {α : Type u_1} :
has_ssubset (finset α)
Equations
source
@[protected, instance]
def finset.partial_order {α : Type u_1} :
partial_order (finset α)
Equations
source
@[protected, instance]
def finset.has_subset.subset.is_refl {α : Type u_1} :
is_refl (finset α) has_subset.subset
source
@[protected, instance]
def finset.has_subset.subset.is_trans {α : Type u_1} :
is_trans (finset α) has_subset.subset
source
@[protected, instance]
def finset.has_subset.subset.is_antisymm {α : Type u_1} :
is_antisymm (finset α) has_subset.subset
source
@[protected, instance]
def finset.has_ssubset.ssubset.is_irrefl {α : Type u_1} :
is_irrefl (finset α) has_ssubset.ssubset
source
@[protected, instance]
def finset.has_ssubset.ssubset.is_trans {α : Type u_1} :
is_trans (finset α) has_ssubset.ssubset
source
@[protected, instance]
def finset.has_ssubset.ssubset.is_asymm {α : Type u_1} :
is_asymm (finset α) has_ssubset.ssubset
source
@[protected, instance]
def finset.has_ssubset.ssubset.is_nonstrict_strict_order {α : Type u_1} :
is_nonstrict_strict_order (finset α) has_subset.subset has_ssubset.ssubset
Equations
source
theorem finset.subset_def {α : Type u_1} {s t : finset α} :
s ⊆ t ↔ s.val ⊆ t.val
source
theorem finset.ssubset_def {α : Type u_1} {s t : finset α} :
s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s
source
@[simp]
theorem finset.subset.refl {α : Type u_1} (s : finset α) :
s ⊆ s
source
@[protected]
theorem finset.subset.rfl {α : Type u_1} {s : finset α} :
s ⊆ s
source
@[protected]
theorem finset.subset_of_eq {α : Type u_1} {s t : finset α} (h : s = t) :
s ⊆ t
source
theorem finset.subset.trans {α : Type u_1} {s₁ s₂ s₃ : finset α} :
s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃
source
theorem finset.superset.trans {α : Type u_1} {s₁ s₂ s₃ : finset α} :
s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃
source
theorem finset.mem_of_subset {α : Type u_1} {s₁ s₂ : finset α} {a : α} :
s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂
source
theorem finset.not_mem_mono {α : Type u_1} {s t : finset α} (h : s ⊆ t) {a : α} :
a ∉ t → a ∉ s
source
theorem finset.subset.antisymm {α : Type u_1} {s₁ s₂ : finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) :
s₁ = s₂
source
theorem finset.subset_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂
source
@[simp, norm_cast]
theorem finset.coe_subset {α : Type u_1} {s₁ s₂ : finset α} :
↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂
source
@[simp]
theorem finset.val_le_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂
source
theorem finset.subset.antisymm_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁
source
theorem finset.not_subset {α : Type u_1} {s t : finset α} :
¬s ⊆ t ↔ ∃ (x : α) (H : x ∈ s), x ∉ t
source
@[simp]
theorem finset.le_eq_subset {α : Type u_1} :
has_le.le = has_subset.subset
source
@[simp]
theorem finset.lt_eq_subset {α : Type u_1} :
has_lt.lt = has_ssubset.ssubset
source
theorem finset.le_iff_subset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ ≤ s₂ ↔ s₁ ⊆ s₂
source
theorem finset.lt_iff_ssubset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ < s₂ ↔ s₁ ⊂ s₂
source
@[simp, norm_cast]
theorem finset.coe_ssubset {α : Type u_1} {s₁ s₂ : finset α} :
↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂
source
@[simp]
theorem finset.val_lt_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁.val < s₂.val ↔ s₁ ⊂ s₂
source
theorem finset.ssubset_iff_subset_ne {α : Type u_1} {s t : finset α} :
s ⊂ t ↔ s ⊆ t ∧ s ≠ t
source
theorem finset.ssubset_iff_of_subset {α : Type u_1} {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) :
s₁ ⊂ s₂ ↔ ∃ (x : α) (H : x ∈ s₂), x ∉ s₁
source
theorem finset.ssubset_of_ssubset_of_subset {α : Type u_1} {s₁ s₂ s₃ : finset α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) :
s₁ ⊂ s₃
source
theorem finset.ssubset_of_subset_of_ssubset {α : Type u_1} {s₁ s₂ s₃ : finset α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) :
s₁ ⊂ s₃
source
theorem finset.exists_of_ssubset {α : Type u_1} {s₁ s₂ : finset α} (h : s₁ ⊂ s₂) :
∃ (x : α) (H : x ∈ s₂), x ∉ s₁
source
@[protected, instance]
def finset.is_well_founded_ssubset {α : Type u_1} :
is_well_founded (finset α) has_ssubset.ssubset
source
@[protected, instance]
def finset.is_well_founded_lt {α : Type u_1} :
well_founded_lt (finset α)

Order embedding from finset α to set α #

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

Coercion to set α as an order_embedding.

Equations
source
@[simp]
theorem finset.coe_coe_emb {α : Type u_1} :
⇑finset.coe_emb = coe

Nonempty #

source
@[protected]
def finset.nonempty {α : Type u_1} (s : finset α) :
Prop

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

Equations
Instances for finset.nonempty
source
@[protected, instance]
def finset.decidable_nonempty {α : Type u_1} {s : finset α} :
decidable s.nonempty
Equations
source
@[simp, norm_cast]
theorem finset.coe_nonempty {α : Type u_1} {s : finset α} :
↑s.nonempty ↔ s.nonempty
source
@[simp]
theorem finset.nonempty_coe_sort {α : Type u_1} {s : finset α} :
nonempty ↥s ↔ s.nonempty
source
theorem finset.nonempty.to_set {α : Type u_1} {s : finset α} :
s.nonempty → ↑s.nonempty

Alias of the reverse direction of finset.coe_nonempty.

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

Alias of the reverse direction of finset.nonempty_coe_sort.

source
theorem finset.nonempty.bex {α : Type u_1} {s : finset α} (h : s.nonempty) :
∃ (x : α), x ∈ s
source
theorem finset.nonempty.mono {α : Type u_1} {s t : finset α} (hst : s ⊆ t) (hs : s.nonempty) :
t.nonempty
source
theorem finset.nonempty.forall_const {α : Type u_1} {s : finset α} (h : s.nonempty) {p : Prop} :
(∀ (x : α), x ∈ s → p) ↔ p
source
theorem finset.nonempty.to_subtype {α : Type u_1} {s : finset α} :
s.nonempty → nonempty ↥s
source
theorem finset.nonempty.to_type {α : Type u_1} {s : finset α} :
s.nonempty → nonempty α

empty #

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

The empty finset

Equations
source
@[protected, instance]
def finset.has_emptyc {α : Type u_1} :
has_emptyc (finset α)
Equations
source
@[protected, instance]
def finset.inhabited_finset {α : Type u_1} :
inhabited (finset α)
Equations
source
@[simp]
theorem finset.empty_val {α : Type u_1} :
∅.val = 0
source
@[simp]
theorem finset.not_mem_empty {α : Type u_1} (a : α) :
a ∉ ∅
source
@[simp]
theorem finset.not_nonempty_empty {α : Type u_1} :
¬∅.nonempty
source
@[simp]
theorem finset.mk_zero {α : Type u_1} :
{val := 0, nodup := _} = ∅
source
theorem finset.ne_empty_of_mem {α : Type u_1} {a : α} {s : finset α} (h : a ∈ s) :
s ≠ ∅
source
theorem finset.nonempty.ne_empty {α : Type u_1} {s : finset α} (h : s.nonempty) :
s ≠ ∅
source
@[simp]
theorem finset.empty_subset {α : Type u_1} (s : finset α) :
∅ ⊆ s
source
theorem finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : finset α} (H : ∀ (x : α), x ∉ s) :
s = ∅
source
theorem finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : finset α} :
s = ∅ ↔ ∀ (x : α), x ∉ s
source
@[simp]
theorem finset.val_eq_zero {α : Type u_1} {s : finset α} :
s.val = 0 ↔ s = ∅
source
theorem finset.subset_empty {α : Type u_1} {s : finset α} :
s ⊆ ∅ ↔ s = ∅
source
@[simp]
theorem finset.not_ssubset_empty {α : Type u_1} (s : finset α) :
¬s ⊂ ∅
source
theorem finset.nonempty_of_ne_empty {α : Type u_1} {s : finset α} (h : s ≠ ∅) :
s.nonempty
source
theorem finset.nonempty_iff_ne_empty {α : Type u_1} {s : finset α} :
s.nonempty ↔ s ≠ ∅
source
@[simp]
theorem finset.not_nonempty_iff_eq_empty {α : Type u_1} {s : finset α} :
¬s.nonempty ↔ s = ∅
source
theorem finset.eq_empty_or_nonempty {α : Type u_1} (s : finset α) :
s = ∅ ∨ s.nonempty
source
@[simp, norm_cast]
theorem finset.coe_empty {α : Type u_1} :
↑∅ = ∅
source
@[simp, norm_cast]
theorem finset.coe_eq_empty {α : Type u_1} {s : finset α} :
↑s = ∅ ↔ s = ∅
source
@[simp]
theorem finset.is_empty_coe_sort {α : Type u_1} {s : finset α} :
is_empty ↥s ↔ s = ∅
source
@[protected, instance]
def finset.has_emptyc.emptyc.is_empty {α : Type u_1} :
is_empty ↥∅
source
theorem finset.eq_empty_of_is_empty {α : Type u_1} [is_empty α] (s : finset α) :
s = ∅

A finset for an empty type is empty.

source
@[protected, instance]
def finset.order_bot {α : Type u_1} :
order_bot (finset α)
Equations
source
@[simp]
theorem finset.bot_eq_empty {α : Type u_1} :
⊥ = ∅
source
@[simp]
theorem finset.empty_ssubset {α : Type u_1} {s : finset α} :
∅ ⊂ s ↔ s.nonempty
source
theorem finset.nonempty.empty_ssubset {α : Type u_1} {s : finset α} :
s.nonempty → ∅ ⊂ s

Alias of the reverse direction of finset.empty_ssubset.

singleton #

source
@[protected, instance]
def finset.has_singleton {α : Type u_1} :
has_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 decidable_eq instance for α.

Equations
source
@[simp]
theorem finset.singleton_val {α : Type u_1} (a : α) :
{a}.val = {a}
source
@[simp]
theorem finset.mem_singleton {α : Type u_1} {a b : α} :
b ∈ {a} ↔ b = a
source
theorem finset.eq_of_mem_singleton {α : Type u_1} {x y : α} (h : x ∈ {y}) :
x = y
source
theorem finset.not_mem_singleton {α : Type u_1} {a b : α} :
a ∉ {b} ↔ a ≠ b
source
theorem finset.mem_singleton_self {α : Type u_1} (a : α) :
a ∈ {a}
source
@[simp]
theorem finset.val_eq_singleton_iff {α : Type u_1} {a : α} {s : finset α} :
s.val = {a} ↔ s = {a}
source
theorem finset.singleton_injective {α : Type u_1} :
function.injective has_singleton.singleton
source
@[simp]
theorem finset.singleton_inj {α : Type u_1} {a b : α} :
{a} = {b} ↔ a = b
source
@[simp]
theorem finset.singleton_nonempty {α : Type u_1} (a : α) :
{a}.nonempty
source
@[simp]
theorem finset.singleton_ne_empty {α : Type u_1} (a : α) :
{a} ≠ ∅
source
theorem finset.empty_ssubset_singleton {α : Type u_1} {a : α} :
∅ ⊂ {a}
source
@[simp, norm_cast]
theorem finset.coe_singleton {α : Type u_1} (a : α) :
↑{a} = {a}
source
@[simp, norm_cast]
theorem finset.coe_eq_singleton {α : Type u_1} {s : finset α} {a : α} :
↑s = {a} ↔ s = {a}
source
theorem finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : finset α} {a : α} :
s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
source
theorem finset.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : finset α} {a : α} :
s = {a} ↔ s.nonempty ∧ ∀ (x : α), x ∈ s → x = a
source
theorem finset.nonempty_iff_eq_singleton_default {α : Type u_1} [unique α] {s : finset α} :
s.nonempty ↔ s = {inhabited.default}
source
theorem finset.nonempty.eq_singleton_default {α : Type u_1} [unique α] {s : finset α} :
s.nonempty → s = {inhabited.default}

Alias of the forward direction of finset.nonempty_iff_eq_singleton_default.

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

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

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

cons #

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

Equations
source
@[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
source
@[simp]
theorem finset.mem_cons_self {α : Type u_1} (a : α) (s : finset α) {h : a ∉ s} :
a ∈ finset.cons a s h
source
@[simp]
theorem finset.cons_val {α : Type u_1} {s : finset α} {a : α} (h : a ∉ s) :
(finset.cons a s h).val = a ::ₘ s.val
source
theorem finset.forall_mem_cons {α : Type u_1} {s : finset α} {a : α} (h : a ∉ s) (p : α → Prop) :
(∀ (x : α), x ∈ finset.cons a s h → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
source
theorem finset.forall_of_forall_cons {α : Type u_1} {s : finset α} {a : α} {p : α → Prop} {h : a ∉ s} (H : ∀ (x : α), x ∈ finset.cons a s h → p x) (x : α) (h_1 : x ∈ s) :
p x

Useful in proofs by induction.

source
@[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 := _} _
source
@[simp]
theorem finset.cons_empty {α : Type u_1} (a : α) :
finset.cons a ∅ _ = {a}
source
@[simp]
theorem finset.nonempty_cons {α : Type u_1} {s : finset α} {a : α} (h : a ∉ s) :
(finset.cons a s h).nonempty
source
@[simp]
theorem finset.nonempty_mk {α : Type u_1} {m : multiset α} {hm : m.nodup} :
{val := m, nodup := hm}.nonempty ↔ m ≠ 0
source
@[simp]
theorem finset.coe_cons {α : Type u_1} {a : α} {s : finset α} {h : a ∉ s} :
↑(finset.cons a s h) = has_insert.insert a ↑s
source
theorem finset.subset_cons {α : Type u_1} {s : finset α} {a : α} (h : a ∉ s) :
s ⊆ finset.cons a s h
source
theorem finset.ssubset_cons {α : Type u_1} {s : finset α} {a : α} (h : a ∉ s) :
s ⊂ finset.cons a s h
source
theorem finset.cons_subset {α : Type u_1} {s t : finset α} {a : α} {h : a ∉ s} :
finset.cons a s h ⊆ t ↔ a ∈ t ∧ s ⊆ t
source
@[simp]
theorem finset.cons_subset_cons {α : Type u_1} {s t : finset α} {a : α} {hs : a ∉ s} {ht : a ∉ t} :
finset.cons a s hs ⊆ finset.cons a t ht ↔ s ⊆ t
source
theorem finset.ssubset_iff_exists_cons_subset {α : Type u_1} {s t : finset α} :
s ⊂ t ↔ ∃ (a : α) (h : a ∉ s), finset.cons a s h ⊆ t

disjoint #

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

disjoint union #

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

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

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

insert #

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

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

Equations
source
theorem finset.insert_def {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
has_insert.insert a s = {val := multiset.ndinsert a s.val, nodup := _}
source
@[simp]
theorem finset.insert_val {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(has_insert.insert a s).val = multiset.ndinsert a s.val
source
theorem finset.insert_val' {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(has_insert.insert a s).val = (a ::ₘ s.val).dedup
source
theorem finset.insert_val_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a ∉ s) :
(has_insert.insert a s).val = a ::ₘ s.val
source
@[simp]
theorem finset.mem_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
a ∈ has_insert.insert b s ↔ a = b ∨ a ∈ s
source
theorem finset.mem_insert_self {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
a ∈ has_insert.insert a s
source
theorem finset.mem_insert_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (h : a ∈ s) :
a ∈ has_insert.insert b s
source
theorem finset.mem_of_mem_insert_of_ne {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (h : b ∈ has_insert.insert a s) :
b ≠ a → b ∈ s
source
theorem finset.eq_of_not_mem_of_mem_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (ha : b ∈ has_insert.insert a s) (hb : b ∉ s) :
b = a
source
@[simp]
theorem finset.cons_eq_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) (h : a ∉ s) :
finset.cons a s h = has_insert.insert a s
source
@[simp, norm_cast]
theorem finset.coe_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
↑(has_insert.insert a s) = has_insert.insert a ↑s
source
theorem finset.mem_insert_coe {α : Type u_1} [decidable_eq α] {s : finset α} {x y : α} :
x ∈ has_insert.insert y s ↔ x ∈ has_insert.insert y ↑s
source
@[protected, instance]
def finset.is_lawful_singleton {α : Type u_1} [decidable_eq α] :
is_lawful_singleton α (finset α)
source
@[simp]
theorem finset.insert_eq_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (h : a ∈ s) :
has_insert.insert a s = s
source
@[simp]
theorem finset.insert_eq_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
has_insert.insert a s = s ↔ a ∈ s
source
theorem finset.insert_ne_self {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
has_insert.insert a s ≠ s ↔ a ∉ s
source
@[simp]
theorem finset.pair_eq_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a, a} = {a}
source
theorem finset.insert.comm {α : Type u_1} [decidable_eq α] (a b : α) (s : finset α) :
has_insert.insert a (has_insert.insert b s) = has_insert.insert b (has_insert.insert a s)
source
@[simp, norm_cast]
theorem finset.coe_pair {α : Type u_1} [decidable_eq α] {a b : α} :
↑{a, b} = {a, b}
source
@[simp, norm_cast]
theorem finset.coe_eq_pair {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
↑s = {a, b} ↔ s = {a, b}
source
theorem finset.pair_comm {α : Type u_1} [decidable_eq α] (a b : α) :
{a, b} = {b, a}
source
@[simp]
theorem finset.insert_idem {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
has_insert.insert a (has_insert.insert a s) = has_insert.insert a s
source
@[simp]
theorem finset.insert_nonempty {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(has_insert.insert a s).nonempty
source
@[simp]
theorem finset.insert_ne_empty {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
has_insert.insert a s ≠ ∅

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

source
@[protected, instance]
def finset.has_insert.insert.nonempty {α : Type u} [decidable_eq α] (i : α) (s : finset α) :
nonempty ↥↑(has_insert.insert i s)
source
theorem finset.ne_insert_of_not_mem {α : Type u_1} [decidable_eq α] (s t : finset α) {a : α} (h : a ∉ s) :
s ≠ has_insert.insert a t
source
theorem finset.insert_subset {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
has_insert.insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
source
theorem finset.subset_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s ⊆ has_insert.insert a s
source
theorem finset.insert_subset_insert {α : Type u_1} [decidable_eq α] (a : α) {s t : finset α} (h : s ⊆ t) :
has_insert.insert a s ⊆ has_insert.insert a t
source
theorem finset.insert_inj {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (ha : a ∉ s) :
has_insert.insert a s = has_insert.insert b s ↔ a = b
source
theorem finset.insert_inj_on {α : Type u_1} [decidable_eq α] (s : finset α) :
set.inj_on (λ (a : α), has_insert.insert a s) (↑s)ᶜ
source
theorem finset.ssubset_iff {α : Type u_1} [decidable_eq α] {s t : finset α} :
s ⊂ t ↔ ∃ (a : α) (H : a ∉ s), has_insert.insert a s ⊆ t
source
theorem finset.ssubset_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (h : a ∉ s) :
s ⊂ has_insert.insert a s
source
theorem finset.cons_induction {α : Type u_1} {p : finset α → Prop} (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α} (h : a ∉ s), p s → p (finset.cons a s h)) (s : finset α) :
p s
source
theorem finset.cons_induction_on {α : Type u_1} {p : finset α → Prop} (s : finset α) (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α} (h : a ∉ s), p s → p (finset.cons a s h)) :
p s
source
@[protected]
theorem finset.induction {α : Type u_1} {p : finset α → Prop} [decidable_eq α] (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (has_insert.insert a s)) (s : finset α) :
p s
source
@[protected]
theorem finset.induction_on {α : Type u_1} {p : finset α → Prop} [decidable_eq α] (s : finset α) (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (has_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.

source
theorem finset.induction_on' {α : Type u_1} {p : finset α → Prop} [decidable_eq α] (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a : α} {s : finset α}, a ∈ S → s ⊆ S → a ∉ s → p s → p (has_insert.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.

source
theorem finset.nonempty.cons_induction {α : Type u_1} {p : Π (s : finset α), s.nonempty → Prop} (h₀ : ∀ (a : α), p {a} _) (h₁ : ∀ ⦃a : α⦄ (s : finset α) (h : a ∉ s) (hs : s.nonempty), p s hs → p (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.

source
def finset.subtype_insert_equiv_option {α : Type u_1} [decidable_eq α] {t : finset α} {x : α} (h : x ∉ t) :
{i // i ∈ has_insert.insert x t} ≃ option {i // i ∈ t}

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

Equations
source
@[simp]
theorem finset.disjoint_insert_left {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
disjoint (has_insert.insert a s) t ↔ a ∉ t ∧ disjoint s t
source
@[simp]
theorem finset.disjoint_insert_right {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
disjoint s (has_insert.insert a t) ↔ a ∉ s ∧ disjoint s t

Lattice structure #

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

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

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

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

Equations
source
@[protected, instance]
def finset.lattice {α : Type u_1} [decidable_eq α] :
lattice (finset α)
Equations
source
@[simp]
theorem finset.sup_eq_union {α : Type u_1} [decidable_eq α] :
has_sup.sup = has_union.union
source
@[simp]
theorem finset.inf_eq_inter {α : Type u_1} [decidable_eq α] :
has_inf.inf = has_inter.inter
source
theorem finset.disjoint_iff_inter_eq_empty {α : Type u_1} [decidable_eq α] {s t : finset α} :
disjoint s t ↔ s ∩ t = ∅
source
@[protected, instance]
def finset.decidable_disjoint {α : Type u_1} [decidable_eq α] (U V : finset α) :
decidable (disjoint U V)
Equations

union #

source
theorem finset.union_val_nd {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s ∪ t).val = s.val.ndunion t.val
source
@[simp]
theorem finset.union_val {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s ∪ t).val = s.val ∪ t.val
source
@[simp]
theorem finset.mem_union {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
source
@[simp]
theorem finset.disj_union_eq_union {α : Type u_1} [decidable_eq α] (s t : finset α) (h : disjoint s t) :
s.disj_union t h = s ∪ t
source
theorem finset.mem_union_left {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (t : finset α) (h : a ∈ s) :
a ∈ s ∪ t
source
theorem finset.mem_union_right {α : Type u_1} [decidable_eq α] {t : finset α} {a : α} (s : finset α) (h : a ∈ t) :
a ∈ s ∪ t
source
theorem finset.forall_mem_union {α : Type u_1} [decidable_eq α] {s t : finset α} {p : α → Prop} :
(∀ (a : α), a ∈ s ∪ t → p a) ↔ (∀ (a : α), a ∈ s → p a) ∧ ∀ (a : α), a ∈ t → p a
source
theorem finset.not_mem_union {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t
source
@[simp, norm_cast]
theorem finset.coe_union {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂
source
theorem finset.union_subset {α : Type u_1} [decidable_eq α] {s t u : finset α} (hs : s ⊆ u) :
t ⊆ u → s ∪ t ⊆ u
source
theorem finset.subset_union_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ ⊆ s₁ ∪ s₂
source
theorem finset.subset_union_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₂ ⊆ s₁ ∪ s₂
source
theorem finset.union_subset_union {α : Type u_1} [decidable_eq α] {s t u v : finset α} (hsu : s ⊆ u) (htv : t ⊆ v) :
s ∪ t ⊆ u ∪ v
source
theorem finset.union_subset_union_left {α : Type u_1} [decidable_eq α] {s₁ s₂ t : finset α} (h : s₁ ⊆ s₂) :
s₁ ∪ t ⊆ s₂ ∪ t
source
theorem finset.union_subset_union_right {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} (h : t₁ ⊆ t₂) :
s ∪ t₁ ⊆ s ∪ t₂
source
theorem finset.union_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ ∪ s₂ = s₂ ∪ s₁
source
@[protected, instance]
def finset.has_union.union.is_commutative {α : Type u_1} [decidable_eq α] :
is_commutative (finset α) has_union.union
source
@[simp]
theorem finset.union_assoc {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
source
@[protected, instance]
def finset.has_union.union.is_associative {α : Type u_1} [decidable_eq α] :
is_associative (finset α) has_union.union
source
@[simp]
theorem finset.union_idempotent {α : Type u_1} [decidable_eq α] (s : finset α) :
s ∪ s = s
source
@[protected, instance]
def finset.has_union.union.is_idempotent {α : Type u_1} [decidable_eq α] :
is_idempotent (finset α) has_union.union
source
theorem finset.union_subset_left {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : s ∪ t ⊆ u) :
s ⊆ u
source
theorem finset.union_subset_right {α : Type u_1} [decidable_eq α] {s t u : finset α} (h : s ∪ t ⊆ u) :
t ⊆ u
source
theorem finset.union_left_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s ∪ (t ∪ u) = t ∪ (s ∪ u)
source
theorem finset.union_right_comm {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s ∪ t ∪ u = s ∪ u ∪ t
source
theorem finset.union_self {α : Type u_1} [decidable_eq α] (s : finset α) :
s ∪ s = s
source
@[simp]
theorem finset.union_empty {α : Type u_1} [decidable_eq α] (s : finset α) :
s ∪ ∅ = s
source
@[simp]
theorem finset.empty_union {α : Type u_1} [decidable_eq α] (s : finset α) :
∅ ∪ s = s
source
theorem finset.insert_eq {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
has_insert.insert a s = {a} ∪ s
source
@[simp]
theorem finset.insert_union {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
has_insert.insert a s ∪ t = has_insert.insert a (s ∪ t)
source
@[simp]
theorem finset.union_insert {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
s ∪ has_insert.insert a t = has_insert.insert a (s ∪ t)
source
theorem finset.insert_union_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
has_insert.insert a (s ∪ t) = has_insert.insert a s ∪ has_insert.insert a t
source
@[simp]
theorem finset.union_eq_left_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s ∪ t = s ↔ t ⊆ s
source
@[simp]
theorem finset.left_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s = s ∪ t ↔ t ⊆ s
source
@[simp]
theorem finset.union_eq_right_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s ∪ t = t ↔ s ⊆ t
source
@[simp]
theorem finset.right_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s = t ∪ s ↔ t ⊆ s
source
theorem finset.union_congr_left {α : Type u_1} [decidable_eq α] {s t u : finset α} (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) :
s ∪ t = s ⊔ u
source
theorem finset.union_congr_right {α : Type u_1} [decidable_eq α] {s t u : finset α} (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) :
s ∪ u = t ∪ u
source
theorem finset.union_eq_union_iff_left {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
source
theorem finset.union_eq_union_iff_right {α : Type u_1} [decidable_eq α] {s t u : finset α} :
s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
source
@[simp]
theorem finset.disjoint_union_left {α : Type u_1} [decidable_eq α] {s t u : finset α} :
disjoint (s ∪ t) u ↔ disjoint s u ∧ disjoint t u
source
@[simp]
theorem finset.disjoint_union_right {α : Type u_1} [decidable_eq α] {s t u : finset α} :
disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u
source
theorem finset.induction_on_union {α : Type u_1} [decidable_eq α] (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 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].
source
theorem directed.exists_mem_subset_of_finset_subset_bUnion {α : Type u_1} {ι : Type u_2} [hn : nonempty ι] {f : ι → set α} (h : directed has_subset.subset f) {s : finset α} (hs : ↑s ⊆ ⋃ (i : ι), f i) :
∃ (i : ι), ↑s ⊆ f i
source
theorem directed_on.exists_mem_subset_of_finset_subset_bUnion {α : Type u_1} {ι : Type u_2} {f : ι → set α} {c : set ι} (hn : c.nonempty) (hc : directed_on (λ (i j : ι), f i ⊆ f j) c) {s : finset α} (hs : ↑s ⊆ ⋃ (i : ι) (H : i ∈ c), f i) :
∃ (i : ι) (H : i ∈ c), ↑s ⊆ f i

inter #

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

Alias of the reverse direction of finset.not_disjoint_iff_nonempty_inter.

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

erase #

source
def finset.erase {α : Type u_1} [decidable_eq α] (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
source
@[simp]
theorem finset.erase_val {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
(s.erase a).val = s.val.erase a
source
@[simp]
theorem finset.mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s
source
theorem finset.not_mem_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
a ∉ s.erase a
source
@[simp, nolint]
theorem finset.erase_empty {α : Type u_1} [decidable_eq α] (a : α) :
∅.erase a = ∅
source
@[simp]
theorem finset.erase_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.erase a = ∅
source
theorem finset.ne_of_mem_erase {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
b ∈ s.erase a → b ≠ a
source
theorem finset.mem_of_mem_erase {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
b ∈ s.erase a → b ∈ s
source
theorem finset.mem_erase_of_ne_of_mem {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
a ≠ b → a ∈ s → a ∈ s.erase b
source
theorem finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} (hs : b ∈ s) (hsa : b ∉ s.erase a) :
b = a

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

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

sdiff #

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

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

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

Symmetric difference #

source
theorem finset.mem_symm_diff {α : Type u_1} [decidable_eq α] {s t : finset α} {a : α} :
a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
source
@[simp, norm_cast]
theorem finset.coe_symm_diff {α : Type u_1} [decidable_eq α] {s t : finset α} :
↑(s ∆ t) = ↑s ∆ ↑t

attach #

source
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
source
theorem finset.sizeof_lt_sizeof_of_mem {α : Type u_1} [has_sizeof α] {x : α} {s : finset α} (hx : x ∈ s) :
sizeof x < sizeof s
source
@[simp]
theorem finset.attach_val {α : Type u_1} (s : finset α) :
s.attach.val = s.val.attach
source
@[simp]
theorem finset.mem_attach {α : Type u_1} (s : finset α) (x : {x // x ∈ s}) :
x ∈ s.attach
source
@[simp]
theorem finset.attach_empty {α : Type u_1} :
∅.attach = ∅
source
@[simp]
theorem finset.attach_nonempty_iff {α : Type u_1} {s : finset α} :
s.attach.nonempty ↔ s.nonempty
source
@[simp]
theorem finset.attach_eq_empty_iff {α : Type u_1} {s : finset α} :
s.attach = ∅ ↔ s = ∅

piecewise #

source
def finset.piecewise {α : Type u_1} {δ : α → Sort u_2} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] (i : α) :
δ i

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

Equations
source
@[simp]
theorem finset.piecewise_insert_self {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [decidable_eq α] {j : α} [Π (i : α), decidable (i ∈ has_insert.insert j s)] :
(has_insert.insert j s).piecewise f g j = f j
source
@[simp]
theorem finset.piecewise_empty {α : Type u_1} {δ : α → Sort u_4} (f g : Π (i : α), δ i) [Π (i : α), decidable (i ∈ ∅)] :
∅.piecewise f g = g
source
@[norm_cast]
theorem finset.piecewise_coe {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [Π (j : α), decidable (j ∈ ↑s)] :
↑s.piecewise f g = s.piecewise f g
source
@[simp]
theorem finset.piecewise_eq_of_mem {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] {i : α} (hi : i ∈ s) :
s.piecewise f g i = f i
source
@[simp]
theorem finset.piecewise_eq_of_not_mem {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] {i : α} (hi : i ∉ s) :
s.piecewise f g i = g i
source
theorem finset.piecewise_congr {α : Type u_1} {δ : α → Sort u_4} (s : finset α) [Π (j : α), decidable (j ∈ s)] {f f' g g' : Π (i : α), δ i} (hf : ∀ (i : α), i ∈ s → f i = f' i) (hg : ∀ (i : α), i ∉ s → g i = g' i) :
s.piecewise f g = s.piecewise f' g'
source
@[simp]
theorem finset.piecewise_insert_of_ne {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [decidable_eq α] {i j : α} [Π (i : α), decidable (i ∈ has_insert.insert j s)] (h : i ≠ j) :
(has_insert.insert j s).piecewise f g i = s.piecewise f g i
source
theorem finset.piecewise_insert {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [decidable_eq α] (j : α) [Π (i : α), decidable (i ∈ has_insert.insert j s)] :
(has_insert.insert j s).piecewise f g = function.update (s.piecewise f g) j (f j)
source
theorem finset.piecewise_cases {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] {i : α} (p : δ i → Prop) (hf : p (f i)) (hg : p (g i)) :
p (s.piecewise f g i)
source
theorem finset.piecewise_mem_set_pi {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} {t : set α} {t' : Π (i : α), set (δ i)} {f g : Π (i : α), δ i} (hf : f ∈ t.pi t') (hg : g ∈ t.pi t') :
s.piecewise f g ∈ t.pi t'
source
theorem finset.piecewise_singleton {α : Type u_1} {δ : α → Sort u_4} (f g : Π (i : α), δ i) [decidable_eq α] (i : α) :
{i}.piecewise f g = function.update g i (f i)
source
theorem finset.piecewise_piecewise_of_subset_left {α : Type u_1} {δ : α → Sort u_4} {s t : finset α} [Π (i : α), decidable (i ∈ s)] [Π (i : α), decidable (i ∈ t)] (h : s ⊆ t) (f₁ f₂ g : Π (a : α), δ a) :
s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g
source
@[simp]
theorem finset.piecewise_idem_left {α : Type u_1} {δ : α → Sort u_4} (s : finset α) [Π (j : α), decidable (j ∈ s)] (f₁ f₂ g : Π (a : α), δ a) :
s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g
source
theorem finset.piecewise_piecewise_of_subset_right {α : Type u_1} {δ : α → Sort u_4} {s t : finset α} [Π (i : α), decidable (i ∈ s)] [Π (i : α), decidable (i ∈ t)] (h : t ⊆ s) (f g₁ g₂ : Π (a : α), δ a) :
s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂
source
@[simp]
theorem finset.piecewise_idem_right {α : Type u_1} {δ : α → Sort u_4} (s : finset α) [Π (j : α), decidable (j ∈ s)] (f g₁ g₂ : Π (a : α), δ a) :
s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂
source
theorem finset.update_eq_piecewise {α : Type u_1} {β : Type u_2} [decidable_eq α] (f : α → β) (i : α) (v : β) :
function.update f i v = {i}.piecewise (λ (j : α), v) f
source
theorem finset.update_piecewise {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [decidable_eq α] (i : α) (v : δ i) :
function.update (s.piecewise f g) i v = s.piecewise (function.update f i v) (function.update g i v)
source
theorem finset.update_piecewise_of_mem {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [decidable_eq α] {i : α} (hi : i ∈ s) (v : δ i) :
function.update (s.piecewise f g) i v = s.piecewise (function.update f i v) g
source
theorem finset.update_piecewise_of_not_mem {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [decidable_eq α] {i : α} (hi : i ∉ s) (v : δ i) :
function.update (s.piecewise f g) i v = s.piecewise f (function.update g i v)
source
theorem finset.piecewise_le_of_le_of_le {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f g h : Π (i : α), δ i} (Hf : f ≤ h) (Hg : g ≤ h) :
s.piecewise f g ≤ h
source
theorem finset.le_piecewise_of_le_of_le {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f g h : Π (i : α), δ i} (Hf : h ≤ f) (Hg : h ≤ g) :
h ≤ s.piecewise f g
source
theorem finset.piecewise_le_piecewise' {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f g f' g' : Π (i : α), δ i} (Hf : ∀ (x : α), x ∈ s → f x ≤ f' x) (Hg : ∀ (x : α), x ∉ s → g x ≤ g' x) :
s.piecewise f g ≤ s.piecewise f' g'
source
theorem finset.piecewise_le_piecewise {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f g f' g' : Π (i : α), δ i} (Hf : f ≤ f') (Hg : g ≤ g') :
s.piecewise f g ≤ s.piecewise f' g'
source
theorem finset.piecewise_mem_Icc_of_mem_of_mem {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f f₁ g g₁ : Π (i : α), δ i} (hf : f ∈ set.Icc f₁ g₁) (hg : g ∈ set.Icc f₁ g₁) :
s.piecewise f g ∈ set.Icc f₁ g₁
source
theorem finset.piecewise_mem_Icc {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f g : Π (i : α), δ i} (h : f ≤ g) :
s.piecewise f g ∈ set.Icc f g
source
theorem finset.piecewise_mem_Icc' {α : Type u_1} (s : finset α) [Π (j : α), decidable (j ∈ s)] {δ : α → Type u_2} [Π (i : α), preorder (δ i)] {f g : Π (i : α), δ i} (h : g ≤ f) :
s.piecewise f g ∈ set.Icc g f
source
@[protected, instance]
def finset.decidable_dforall_finset {α : 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
source
@[protected, instance]
def finset.decidable_eq_pi_finset {α : Type u_1} {s : finset α} {β : α → Type u_2} [h : Π (a : α), decidable_eq (β a)] :
decidable_eq (Π (a : α), a ∈ s → β a)

decidable equality for functions whose domain is bounded by finsets

Equations
source
@[protected, instance]
def finset.decidable_dexists_finset {α : 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

filter #

source
def finset.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) :
finset α

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

Equations
source
@[simp]
theorem finset.filter_val {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) :
(finset.filter p s).val = multiset.filter p s.val
source
@[simp]
theorem finset.filter_subset {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) :
finset.filter p s ⊆ s
source
@[simp]
theorem finset.mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} {a : α} :
a ∈ finset.filter p s ↔ a ∈ s ∧ p a
source
theorem finset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} (x : α) (h : x ∈ finset.filter p s) :
x ∈ s
source
theorem finset.filter_ssubset {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
finset.filter p s ⊂ s ↔ ∃ (x : α) (H : x ∈ s), ¬p x
source
theorem finset.filter_filter {α : Type u_1} (p q : α → Prop) [decidable_pred p] [decidable_pred q] (s : finset α) :
finset.filter q (finset.filter p s) = finset.filter (λ (a : α), p a ∧ q a) s
source
theorem finset.filter_comm {α : Type u_1} (p q : α → Prop) [decidable_pred p] [decidable_pred q] (s : finset α) :
finset.filter q (finset.filter p s) = finset.filter p (finset.filter q s)
source
@[simp]
theorem finset.filter_congr_decidable {α : Type u_1} (s : finset α) (p : α → Prop) (h : decidable_pred p) [decidable_pred p] :
finset.filter p s = finset.filter p s
source
theorem finset.filter_true {α : Type u_1} {h : decidable_pred (λ (a : α), true)} (s : finset α) :
finset.filter (λ (a : α), true) s = s
source
theorem finset.filter_false {α : Type u_1} {h : decidable_pred (λ (a : α), false)} (s : finset α) :
finset.filter (λ (a : α), false) s = ∅
source
theorem finset.filter_eq_self {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
finset.filter p s = s ↔ ∀ ⦃x : α⦄, x ∈ s → p x
source
theorem finset.filter_eq_empty_iff {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
finset.filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x
source
theorem finset.filter_nonempty_iff {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
(finset.filter p s).nonempty ↔ ∃ (a : α) (H : a ∈ s), p a
source
@[simp]
theorem finset.filter_true_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} (h : ∀ (x : α), x ∈ s → p x) :
finset.filter p s = s

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

source
@[simp]
theorem finset.filter_false_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} (h : ∀ (x : α), x ∈ s → ¬p x) :
finset.filter p s = ∅

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

source
@[simp]
theorem finset.filter_const {α : Type u_1} (p : Prop) [decidable p] (s : finset α) :
finset.filter (λ (a : α), p) s = ite p s ∅
source
theorem finset.filter_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {s : finset α} (H : ∀ (x : α), x ∈ s → (p x ↔ q x)) :
finset.filter p s = finset.filter q s
source
theorem finset.filter_empty {α : Type u_1} (p : α → Prop) [decidable_pred p] :
finset.filter p ∅ = ∅
source
theorem finset.filter_subset_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] {s t : finset α} (h : s ⊆ t) :
finset.filter p s ⊆ finset.filter p t
source
theorem finset.monotone_filter_left {α : Type u_1} (p : α → Prop) [decidable_pred p] :
monotone (finset.filter p)
source
theorem finset.monotone_filter_right {α : Type u_1} (s : finset α) ⦃p q : α → Prop⦄ [decidable_pred p] [decidable_pred q] (h : p ≤ q) :
finset.filter p s ≤ finset.filter q s
source
@[simp, norm_cast]
theorem finset.coe_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) :
↑(finset.filter p s) = {x ∈ ↑s | p x}
source
theorem finset.subset_coe_filter_of_subset_forall {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) {t : set α} (h₁ : t ⊆ ↑s) (h₂ : ∀ (x : α), x ∈ t → p x) :
t ⊆ ↑(finset.filter p s)
source
theorem finset.filter_singleton {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) :
finset.filter p {a} = ite (p a) {a} ∅
source
theorem finset.filter_cons_of_pos {α : Type u_1} (p : α → Prop) [decidable_pred 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) _
source
theorem finset.filter_cons_of_neg {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) (s : finset α) (ha : a ∉ s) (hp : ¬p a) :
finset.filter p (finset.cons a s ha) = finset.filter p s
source
theorem finset.disjoint_filter {α : Type u_1} {s : finset α} {p q : α → Prop} [decidable_pred p] [decidable_pred q] :
disjoint (finset.filter p s) (finset.filter q s) ↔ ∀ (x : α), x ∈ s → p x → ¬q x
source
theorem finset.disjoint_filter_filter {α : Type u_1} {s t : finset α} {p q : α → Prop} [decidable_pred p] [decidable_pred q] :
disjoint s t → disjoint (finset.filter p s) (finset.filter q t)
source
theorem finset.disjoint_filter_filter' {α : Type u_1} (s t : finset α) {p q : α → Prop} [decidable_pred p] [decidable_pred q] (h : disjoint p q) :
disjoint (finset.filter p s) (finset.filter q t)
source
theorem finset.disjoint_filter_filter_neg {α : Type u_1} (s t : finset α) (p : α → Prop) [decidable_pred p] [decidable_pred (λ (a : α), ¬p a)] :
disjoint (finset.filter p s) (finset.filter (λ (a : α), ¬p a) t)
source
theorem finset.filter_disj_union {α : Type u_1} (p : α → Prop) [decidable_pred p] (s t : finset α) (h : disjoint s t) :
finset.filter p (s.disj_union t h) = (finset.filter p s).disj_union (finset.filter p t) _
source
theorem finset.filter_cons {α : Type u_1} (p : α → Prop) [decidable_pred p] {a : α} (s : finset α) (ha : a ∉ s) :
finset.filter p (finset.cons a s ha) = (ite (p a) {a} ∅).disj_union (finset.filter p s) _
source
theorem finset.filter_union {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s₁ s₂ : finset α) :
finset.filter p (s₁ ∪ s₂) = finset.filter p s₁ ∪ finset.filter p s₂
source
theorem finset.filter_union_right {α : Type u_1} (p q : α → Prop) [decidable_pred p] [decidable_pred q] [decidable_eq α] (s : finset α) :
finset.filter p s ∪ finset.filter q s = finset.filter (λ (x : α), p x ∨ q x) s
source
theorem finset.filter_mem_eq_inter {α : Type u_1} [decidable_eq α] {s t : finset α} [Π (i : α), decidable (i ∈ t)] :
finset.filter (λ (i : α), i ∈ t) s = s ∩ t
source
theorem finset.filter_inter_distrib {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s t : finset α) :
finset.filter p (s ∩ t) = finset.filter p s ∩ finset.filter p t
source
theorem finset.filter_inter {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s t : finset α) :
finset.filter p s ∩ t = finset.filter p (s ∩ t)
source
theorem finset.inter_filter {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (s t : finset α) :
s ∩ finset.filter p t = finset.filter p (s ∩ t)
source
theorem finset.filter_insert {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (a : α) (s : finset α) :
finset.filter p (has_insert.insert a s) = ite (p a) (has_insert.insert a (finset.filter p s)) (finset.filter p s)
source
theorem finset.filter_erase {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] (a : α) (s : finset α) :
finset.filter p (s.erase a) = (finset.filter p s).erase a
source
theorem finset.filter_or {α : Type u_1} (p q : α → Prop) [decidable_pred p] [decidable_pred q] [decidable_eq α] [decidable_pred (λ (a : α), p a ∨ q a)] (s : finset α) :
finset.filter (λ (a : α), p a ∨ q a) s = finset.filter p s ∪ finset.filter q s
source
theorem finset.filter_and {α : Type u_1} (p q : α → Prop) [decidable_pred p] [decidable_pred q] [decidable_eq α] [decidable_pred (λ (a : α), p a ∧ q a)] (s : finset α) :
finset.filter (λ (a : α), p a ∧ q a) s = finset.filter p s ∩ finset.filter q s
source
theorem finset.filter_not {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] [decidable_pred (λ (a : α), ¬p a)] (s : finset α) :
finset.filter (λ (a : α), ¬p a) s = s \ finset.filter p s
source
theorem finset.sdiff_eq_filter {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ \ s₂ = finset.filter (λ (_x : α), _x ∉ s₂) s₁
source
theorem finset.sdiff_eq_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅
source
theorem finset.subset_union_elim {α : Type u_1} [decidable_eq α] {s : finset α} {t₁ t₂ : set α} (h : ↑s ⊆ t₁ ∪ t₂) :
∃ (s₁ s₂ : finset α), s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁
source
@[protected, instance]
noncomputable def finset.has_sep {α : Type u_1} :
has_sep α (finset α)

The following instance allows us to write {x ∈ s | p x} for finset.filter p s. Since the former notation requires us to define this for all propositions p, and finset.filter only works for decidable propositions, the notation {x ∈ s | p x} is only compatible with classical logic because it uses classical.prop_decidable. We don't want to redo all lemmas of finset.filter for has_sep.sep, so we make sure that simp unfolds the notation {x ∈ s | p x} to finset.filter p s. If p happens to be decidable, the simp-lemma finset.filter_congr_decidable will make sure that finset.filter uses the right instance for decidability.

Equations
source
@[simp]
theorem finset.sep_def {α : Type u_1} (s : finset α) (p : α → Prop) :
{x ∈ s | p x} = finset.filter p s
source
theorem finset.filter_eq {β : Type u_2} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (eq b) s = ite (b ∈ s) {b} ∅

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.

source
theorem finset.filter_eq' {β : Type u_2} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (λ (a : β), a = b) s = ite (b ∈ s) {b} ∅

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.

source
theorem finset.filter_ne {β : Type u_2} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (λ (a : β), b ≠ a) s = s.erase b
source
theorem finset.filter_ne' {β : Type u_2} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (λ (a : β), a ≠ b) s = s.erase b
source
theorem finset.filter_inter_filter_neg_eq {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] [decidable_pred (λ (a : α), ¬p a)] (s t : finset α) :
finset.filter p s ∩ finset.filter (λ (a : α), ¬p a) t = ∅
source
theorem finset.filter_union_filter_of_codisjoint {α : Type u_1} (p q : α → Prop) [decidable_pred p] [decidable_pred q] [decidable_eq α] (s : finset α) (h : codisjoint p q) :
finset.filter p s ∪ finset.filter q s = s
source
theorem finset.filter_union_filter_neg_eq {α : Type u_1} (p : α → Prop) [decidable_pred p] [decidable_eq α] [decidable_pred (λ (a : α), ¬p a)] (s : finset α) :
finset.filter p s ∪ finset.filter (λ (a : α), ¬p a) s = s

range #

source
def finset.range (n : ℕ) :
finset ℕ

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

Equations
source
@[simp]
theorem finset.range_val (n : ℕ) :
(finset.range n).val = multiset.range n
source
@[simp]
theorem finset.mem_range {n m : ℕ} :
m ∈ finset.range n ↔ m < n
source
@[simp, norm_cast]
theorem finset.coe_range (n : ℕ) :
↑(finset.range n) = set.Iio n
source
@[simp]
theorem finset.range_zero  :
finset.range 0 = ∅
source
@[simp]
theorem finset.range_one  :
finset.range 1 = {0}
source
theorem finset.range_succ {n : ℕ} :
finset.range n.succ = has_insert.insert n (finset.range n)
source
theorem finset.range_add_one {n : ℕ} :
finset.range (n + 1) = has_insert.insert n (finset.range n)
source
@[simp]
theorem finset.not_mem_range_self {n : ℕ} :
n ∉ finset.range n
source
@[simp]
theorem finset.self_mem_range_succ (n : ℕ) :
n ∈ finset.range (n + 1)
source
@[simp]
theorem finset.range_subset {n m : ℕ} :
finset.range n ⊆ finset.range m ↔ n ≤ m
source
theorem finset.range_mono  :
monotone finset.range
source
theorem finset.mem_range_succ_iff {a b : ℕ} :
a ∈ finset.range b.succ ↔ a ≤ b
source
theorem finset.mem_range_le {n x : ℕ} (hx : x ∈ finset.range n) :
x ≤ n
source
theorem finset.mem_range_sub_ne_zero {n x : ℕ} (hx : x ∈ finset.range n) :
n - x ≠ 0
source
@[simp]
theorem finset.nonempty_range_iff {n : ℕ} :
(finset.range n).nonempty ↔ n ≠ 0
source
@[simp]
theorem finset.range_eq_empty_iff {n : ℕ} :
finset.range n = ∅ ↔ n = 0
source
theorem finset.nonempty_range_succ {n : ℕ} :
(finset.range (n + 1)).nonempty
source
@[simp]
theorem finset.range_filter_eq {n m : ℕ} :
finset.filter (λ (_x : ℕ), _x = m) (finset.range n) = ite (m < n) {m} ∅
source
theorem finset.exists_mem_empty_iff {α : Type u_1} (p : α → Prop) :
(∃ (x : α), x ∈ ∅ ∧ p x) ↔ false
source
theorem finset.exists_mem_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) (p : α → Prop) :
(∃ (x : α), x ∈ has_insert.insert a s ∧ p x) ↔ p a ∨ ∃ (x : α), x ∈ s ∧ p x
source
theorem finset.forall_mem_empty_iff {α : Type u_1} (p : α → Prop) :
(∀ (x : α), x ∈ ∅ → p x) ↔ true
source
theorem finset.forall_mem_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) (p : α → Prop) :
(∀ (x : α), x ∈ has_insert.insert a s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
source
theorem finset.forall_of_forall_insert {α : Type u_1} [decidable_eq α] {p : α → Prop} {a : α} {s : finset α} (H : ∀ (x : α), x ∈ has_insert.insert a s → p x) (x : α) (h : x ∈ s) :
p x

Useful in proofs by induction.

source
def not_mem_range_equiv (k : ℕ) :
{n // n ∉ multiset.range k} ≃ ℕ

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

Equations
source
@[simp]
theorem coe_not_mem_range_equiv (k : ℕ) :
⇑(not_mem_range_equiv k) = λ (i : {n // n ∉ multiset.range k}), ↑i - k
source
@[simp]
theorem coe_not_mem_range_equiv_symm (k : ℕ) :
⇑((not_mem_range_equiv k).symm) = λ (j : ℕ), ⟨j + k, _⟩

dedup on list and multiset #

source
def multiset.to_finset {α : Type u_1} [decidable_eq α] (s : multiset α) :
finset α

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

Equations
source
@[simp]
theorem multiset.to_finset_val {α : Type u_1} [decidable_eq α] (s : multiset α) :
s.to_finset.val = s.dedup
source
theorem multiset.to_finset_eq {α : Type u_1} [decidable_eq α] {s : multiset α} (n : s.nodup) :
{val := s, nodup := n} = s.to_finset
source
theorem multiset.nodup.to_finset_inj {α : Type u_1} [decidable_eq α] {l l' : multiset α} (hl : l.nodup) (hl' : l'.nodup) (h : l.to_finset = l'.to_finset) :
l = l'
source
@[simp]
theorem multiset.mem_to_finset {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a ∈ s.to_finset ↔ a ∈ s
source
@[simp]
theorem multiset.to_finset_zero {α : Type u_1} [decidable_eq α] :
0.to_finset = ∅
source
@[simp]
theorem multiset.to_finset_cons {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
(a ::ₘ s).to_finset = has_insert.insert a s.to_finset
source
@[simp]
theorem multiset.to_finset_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.to_finset = {a}
source
@[simp]
theorem multiset.to_finset_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(s + t).to_finset = s.to_finset ∪ t.to_finset
source
@[simp]
theorem multiset.to_finset_nsmul {α : Type u_1} [decidable_eq α] (s : multiset α) (n : ℕ) (hn : n ≠ 0) :
(n • s).to_finset = s.to_finset
source
@[simp]
theorem multiset.to_finset_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(s ∩ t).to_finset = s.to_finset ∩ t.to_finset
source
@[simp]
theorem multiset.to_finset_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(s ∪ t).to_finset = s.to_finset ∪ t.to_finset
source
@[simp]
theorem multiset.to_finset_eq_empty {α : Type u_1} [decidable_eq α] {m : multiset α} :
m.to_finset = ∅ ↔ m = 0
source
@[simp]
theorem multiset.to_finset_nonempty {α : Type u_1} [decidable_eq α] {s : multiset α} :
s.to_finset.nonempty ↔ s ≠ 0
source
@[simp]
theorem multiset.to_finset_subset {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s.to_finset ⊆ t.to_finset ↔ s ⊆ t
source
@[simp]
theorem multiset.to_finset_ssubset {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s.to_finset ⊂ t.to_finset ↔ s ⊂ t
source
@[simp]
theorem multiset.to_finset_dedup {α : Type u_1} [decidable_eq α] (m : multiset α) :
m.dedup.to_finset = m.to_finset
source
@[simp]
theorem multiset.to_finset_bind_dedup {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (m : multiset α) (f : α → multiset β) :
(m.dedup.bind f).to_finset = (m.bind f).to_finset
source
@[protected, instance]
def multiset.is_well_founded_ssubset {β : Type u_2} :
is_well_founded (multiset β) has_ssubset.ssubset
source
@[simp]
theorem finset.val_to_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
s.val.to_finset = s
source
theorem finset.val_le_iff_val_subset {α : Type u_1} {a : finset α} {b : multiset α} :
a.val ≤ b ↔ a.val ⊆ b
source
def list.to_finset {α : Type u_1} [decidable_eq α] (l : list α) :
finset α

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

Equations
source
@[simp]
theorem list.to_finset_val {α : Type u_1} [decidable_eq α] (l : list α) :
l.to_finset.val = ↑(l.dedup)
source
@[simp]
theorem list.to_finset_coe {α : Type u_1} [decidable_eq α] (l : list α) :
↑l.to_finset = l.to_finset
source
theorem list.to_finset_eq {α : Type u_1} [decidable_eq α] {l : list α} (n : l.nodup) :
{val := ↑l, nodup := n} = l.to_finset
source
@[simp]
theorem list.mem_to_finset {α : Type u_1} [decidable_eq α] {l : list α} {a : α} :
a ∈ l.to_finset ↔ a ∈ l
source
@[simp, norm_cast]
theorem list.coe_to_finset {α : Type u_1} [decidable_eq α] (l : list α) :
↑(l.to_finset) = {a : α | a ∈ l}
source
@[simp]
theorem list.to_finset_nil {α : Type u_1} [decidable_eq α] :
list.nil.to_finset = ∅
source
@[simp]
theorem list.to_finset_cons {α : Type u_1} [decidable_eq α] {l : list α} {a : α} :
(a :: l).to_finset = has_insert.insert a l.to_finset
source
theorem list.to_finset_surj_on {α : Type u_1} [decidable_eq α] :
set.surj_on list.to_finset {l : list α | l.nodup} set.univ
source
theorem list.to_finset_surjective {α : Type u_1} [decidable_eq α] :
function.surjective list.to_finset
source
theorem list.to_finset_eq_iff_perm_dedup {α : Type u_1} [decidable_eq α] {l l' : list α} :
l.to_finset = l'.to_finset ↔ l.dedup ~ l'.dedup
source
theorem list.to_finset.ext_iff {α : Type u_1} [decidable_eq α] {a b : list α} :
a.to_finset = b.to_finset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
source
theorem list.to_finset.ext {α : Type u_1} [decidable_eq α] {l l' : list α} :
(∀ (x : α), x ∈ l ↔ x ∈ l') → l.to_finset = l'.to_finset
source
theorem list.to_finset_eq_of_perm {α : Type u_1} [decidable_eq α] (l l' : list α) (h : l ~ l') :
l.to_finset = l'.to_finset
source
theorem list.perm_of_nodup_nodup_to_finset_eq {α : Type u_1} [decidable_eq α] {l l' : list α} (hl : l.nodup) (hl' : l'.nodup) (h : l.to_finset = l'.to_finset) :
l ~ l'
source
@[simp]
theorem list.to_finset_append {α : Type u_1} [decidable_eq α] {l l' : list α} :
(l ++ l').to_finset = l.to_finset ∪ l'.to_finset
source
@[simp]
theorem list.to_finset_reverse {α : Type u_1} [decidable_eq α] {l : list α} :
l.reverse.to_finset = l.to_finset
source
theorem list.to_finset_replicate_of_ne_zero {α : Type u_1} [decidable_eq α] {a : α} {n : ℕ} (hn : n ≠ 0) :
(list.replicate n a).to_finset = {a}
source
@[simp]
theorem list.to_finset_union {α : Type u_1} [decidable_eq α] (l l' : list α) :
(l ∪ l').to_finset = l.to_finset ∪ l'.to_finset
source
@[simp]
theorem list.to_finset_inter {α : Type u_1} [decidable_eq α] (l l' : list α) :
(l ∩ l').to_finset = l.to_finset ∩ l'.to_finset
source
@[simp]
theorem list.to_finset_eq_empty_iff {α : Type u_1} [decidable_eq α] (l : list α) :
l.to_finset = ∅ ↔ l = list.nil
source
@[simp]
theorem list.to_finset_nonempty_iff {α : Type u_1} [decidable_eq α] (l : list α) :
l.to_finset.nonempty ↔ l ≠ list.nil
source
noncomputable def finset.to_list {α : Type u_1} (s : finset α) :
list α

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

Equations
source
theorem finset.nodup_to_list {α : Type u_1} (s : finset α) :
s.to_list.nodup
source
@[simp]
theorem finset.mem_to_list {α : Type u_1} {a : α} {s : finset α} :
a ∈ s.to_list ↔ a ∈ s
source
@[simp]
theorem finset.to_list_eq_nil {α : Type u_1} {s : finset α} :
s.to_list = list.nil ↔ s = ∅
source
@[simp]
theorem finset.empty_to_list {α : Type u_1} {s : finset α} :
↥(s.to_list.empty) ↔ s = ∅
source
@[simp]
theorem finset.to_list_empty {α : Type u_1} :
∅.to_list = list.nil
source
theorem finset.nonempty.to_list_ne_nil {α : Type u_1} {s : finset α} (hs : s.nonempty) :
s.to_list ≠ list.nil
source
theorem finset.nonempty.not_empty_to_list {α : Type u_1} {s : finset α} (hs : s.nonempty) :
¬↥(s.to_list.empty)
source
@[simp, norm_cast]
theorem finset.coe_to_list {α : Type u_1} (s : finset α) :
↑(s.to_list) = s.val
source
@[simp]
theorem finset.to_list_to_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
s.to_list.to_finset = s
source
@[simp]
theorem finset.to_list_eq_singleton_iff {α : Type u_1} {a : α} {s : finset α} :
s.to_list = [a] ↔ s = {a}
source
@[simp]
theorem finset.to_list_singleton {α : Type u_1} (a : α) :
{a}.to_list = [a]
source
theorem finset.exists_list_nodup_eq {α : Type u_1} [decidable_eq α] (s : finset α) :
∃ (l : list α), l.nodup ∧ l.to_finset = s
source
theorem finset.to_list_cons {α : Type u_1} {a : α} {s : finset α} (h : a ∉ s) :
(finset.cons a s h).to_list ~ a :: s.to_list
source
theorem finset.to_list_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} (h : a ∉ s) :
(has_insert.insert a s).to_list ~ a :: s.to_list

disj_Union #

This section is about the bounded union of a disjoint indexed family t : α → finset β of finite sets over a finite set s : finset α. In most cases finset.bUnion should be preferred.

source
def finset.disj_Union {α : Type u_1} {β : Type u_2} (s : finset α) (t : α → finset β) (hf : ↑s.pairwise_disjoint t) :
finset β

disj_Union s f h is the set such that a ∈ disj_Union s f iff a ∈ f i for some i ∈ s. It is the same as s.bUnion f, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

Equations
source
@[simp]
theorem finset.disj_Union_val {α : Type u_1} {β : Type u_2} (s : finset α) (t : α → finset β) (h : ↑s.pairwise_disjoint t) :
(s.disj_Union t h).val = s.val.bind (λ (a : α), (t a).val)
source
@[simp]
theorem finset.disj_Union_empty {α : Type u_1} {β : Type u_2} (t : α → finset β) :
∅.disj_Union t _ = ∅
source
@[simp]
theorem finset.mem_disj_Union {α : Type u_1} {β : Type u_2} {s : finset α} {t : α → finset β} {b : β} {h : ↑s.pairwise_disjoint t} :
b ∈ s.disj_Union t h ↔ ∃ (a : α) (H : a ∈ s), b ∈ t a
source
@[simp, norm_cast]
theorem finset.coe_disj_Union {α : Type u_1} {β : Type u_2} {s : finset α} {t : α → finset β} {h : ↑s.pairwise_disjoint t} :
↑(s.disj_Union t h) = ⋃ (x : α) (H : x ∈ ↑s), ↑(t x)
source
@[simp]
theorem finset.disj_Union_cons {α : Type u_1} {β : Type u_2} (a : α) (s : finset α) (ha : a ∉ s) (f : α → finset β) (H : ↑(finset.cons a s ha).pairwise_disjoint f) :
(finset.cons a s ha).disj_Union f H = (f a).disj_union (s.disj_Union f _) _
source
@[simp]
theorem finset.singleton_disj_Union {α : Type u_1} {β : Type u_2} {t : α → finset β} (a : α) {h : ↑{a}.pairwise_disjoint t} :
{a}.disj_Union t h = t a
source
theorem finset.disj_Union_disj_Union {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : finset α) (f : α → finset β) (g : β → finset γ) (h1 : ↑s.pairwise_disjoint f) (h2 : ↑(s.disj_Union f h1).pairwise_disjoint g) :
(s.disj_Union f h1).disj_Union g h2 = s.attach.disj_Union (λ (a : {x // x ∈ s}), (f ↑a).disj_Union g _) _
source
theorem finset.disj_Union_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : finset β} {f : α → β} (h : ∀ (x : α), x ∈ s → f x ∈ t) :
t.disj_Union (λ (a : β), finset.filter (λ (c : α), f c = a) s) _ = s

bUnion #

This section is about the bounded union of an indexed family t : α → finset β of finite sets over a finite set s : finset α.

source
@[protected]
def finset.bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (t : α → finset β) :
finset β

bUnion s t is the union of t x over x ∈ s. (This was formerly bind due to the monad structure on types with decidable_eq.)

Equations
source
@[simp]
theorem finset.bUnion_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (t : α → finset β) :
(s.bUnion t).val = (s.val.bind (λ (a : α), (t a).val)).dedup
source
@[simp]
theorem finset.bUnion_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {t : α → finset β} :
∅.bUnion t = ∅
source
@[simp]
theorem finset.mem_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} {b : β} :
b ∈ s.bUnion t ↔ ∃ (a : α) (H : a ∈ s), b ∈ t a
source
@[simp, norm_cast]
theorem finset.coe_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} :
↑(s.bUnion t) = ⋃ (x : α) (H : x ∈ ↑s), ↑(t x)
source
@[simp]
theorem finset.bUnion_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} [decidable_eq α] {a : α} :
(has_insert.insert a s).bUnion t = t a ∪ s.bUnion t
source
theorem finset.bUnion_congr {α : Type u_1} {β : Type u_2} [decidable_eq β] {s₁ s₂ : finset α} {t₁ t₂ : α → finset β} (hs : s₁ = s₂) (ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a) :
s₁.bUnion t₁ = s₂.bUnion t₂
source
@[simp]
theorem finset.disj_Union_eq_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → finset β) (hf : ↑s.pairwise_disjoint f) :
s.disj_Union f hf = s.bUnion f
source
theorem finset.bUnion_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} {s' : finset β} :
s.bUnion t ⊆ s' ↔ ∀ (x : α), x ∈ s → t x ⊆ s'
source
@[simp]
theorem finset.singleton_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] {t : α → finset β} {a : α} :
{a}.bUnion t = t a
source
theorem finset.bUnion_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → finset β) (t : finset β) :
s.bUnion f ∩ t = s.bUnion (λ (x : α), f x ∩ t)
source
theorem finset.inter_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] (t : finset β) (s : finset α) (f : α → finset β) :
t ∩ s.bUnion f = s.bUnion (λ (x : α), t ∩ f x)
source
theorem finset.bUnion_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] (s : finset α) (f : α → finset β) (g : β → finset γ) :
(s.bUnion f).bUnion g = s.bUnion (λ (a : α), (f a).bUnion g)
source
theorem finset.bind_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (s : multiset α) (t : α → multiset β) :
(s.bind t).to_finset = s.to_finset.bUnion (λ (a : α), (t a).to_finset)
source
theorem finset.bUnion_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t₁ t₂ : α → finset β} (h : ∀ (a : α), a ∈ s → t₁ a ⊆ t₂ a) :
s.bUnion t₁ ⊆ s.bUnion t₂
source
theorem finset.bUnion_subset_bUnion_of_subset_left {α : Type u_1} {β : Type u_2} [decidable_eq β] {s₁ s₂ : finset α} (t : α → finset β) (h : s₁ ⊆ s₂) :
s₁.bUnion t ⊆ s₂.bUnion t
source
theorem finset.subset_bUnion_of_mem {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (u : α → finset β) {x : α} (xs : x ∈ s) :
u x ⊆ s.bUnion u
source
@[simp]
theorem finset.bUnion_subset_iff_forall_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : finset β} {f : α → finset β} :
s.bUnion f ⊆ t ↔ ∀ (x : α), x ∈ s → f x ⊆ t
source
@[simp]
theorem finset.bUnion_singleton_eq_self {α : Type u_1} {s : finset α} [decidable_eq α] :
s.bUnion has_singleton.singleton = s
source
theorem finset.filter_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → finset β) (p : β → Prop) [decidable_pred p] :
finset.filter p (s.bUnion f) = s.bUnion (λ (a : α), finset.filter p (f a))
source
theorem finset.bUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {s : finset α} {t : finset β} {f : α → β} (h : ∀ (x : α), x ∈ s → f x ∈ t) :
t.bUnion (λ (a : β), finset.filter (λ (c : α), f c = a) s) = s
source
theorem finset.erase_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → finset β) (s : finset α) (b : β) :
(s.bUnion f).erase b = s.bUnion (λ (x : α), (f x).erase b)
source
@[simp]
theorem finset.bUnion_nonempty {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} :
(s.bUnion t).nonempty ↔ ∃ (x : α) (H : x ∈ s), (t x).nonempty
source
theorem finset.nonempty.bUnion {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} (hs : s.nonempty) (ht : ∀ (x : α), x ∈ s → (t x).nonempty) :
(s.bUnion t).nonempty
source
theorem finset.disjoint_bUnion_left {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → finset β) (t : finset β) :
disjoint (s.bUnion f) t ↔ ∀ (i : α), i ∈ s → disjoint (f i) t
source
theorem finset.disjoint_bUnion_right {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset β) (t : finset α) (f : α → finset β) :
disjoint s (t.bUnion f) ↔ ∀ (i : α), i ∈ t → disjoint s (f i)

choose #

source
def finset.choose_x {α : Type u_1} (p : α → Prop) [decidable_pred 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
source
def finset.choose {α : Type u_1} (p : α → Prop) [decidable_pred 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
source
theorem finset.choose_spec {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : finset α) (hp : ∃! (a : α), a ∈ l ∧ p a) :
finset.choose p l hp ∈ l ∧ p (finset.choose p l hp)
source
theorem finset.choose_mem {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : finset α) (hp : ∃! (a : α), a ∈ l ∧ p a) :
finset.choose p l hp ∈ l
source
theorem finset.choose_property {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : finset α) (hp : ∃! (a : α), a ∈ l ∧ p a) :
p (finset.choose p l hp)
source
theorem finset.pairwise_subtype_iff_pairwise_finset' {α : Type u_1} {β : Type u_2} {s : finset α} (r : β → β → Prop) (f : α → β) :
pairwise (r on λ (x : ↥s), f ↑x) ↔ ↑s.pairwise (r on f)
source
theorem finset.pairwise_subtype_iff_pairwise_finset {α : Type u_1} {s : finset α} (r : α → α → Prop) :
pairwise (r on λ (x : ↥s), ↑x) ↔ ↑s.pairwise r
source
theorem finset.pairwise_cons' {α : Type u_1} {β : Type u_2} {s : finset α} {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) :
pairwise (r on λ (a_1 : ↥(finset.cons a s ha)), f ↑a_1) ↔ pairwise (r on λ (a : ↥s), f ↑a) ∧ ∀ (b : α), b ∈ s → r (f a) (f b) ∧ r (f b) (f a)
source
theorem finset.pairwise_cons {α : Type u_1} {s : finset α} {a : α} (ha : a ∉ s) (r : α → α → Prop) :
pairwise (r on λ (a_1 : ↥(finset.cons a s ha)), ↑a_1) ↔ pairwise (r on λ (a : ↥s), ↑a) ∧ ∀ (b : α), b ∈ s → r a b ∧ r b a
source
def equiv.sigma_equiv_option_of_inhabited (α : Type u) [inhabited α] [decidable_eq α] :
Σ (β : Type u), α ≃ option β

Inhabited types are equivalent to option β for some β by identifying default α with none.

Equations
source
theorem multiset.disjoint_to_finset {α : Type u_1} [decidable_eq α] {m1 m2 : multiset α} :
disjoint m1.to_finset m2.to_finset ↔ m1.disjoint m2
source
theorem list.disjoint_to_finset_iff_disjoint {α : Type u_1} [decidable_eq α] {l l' : list α} :
disjoint l.to_finset l'.to_finset ↔ l.disjoint l'