mathlib docs: data.finset.basic

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

Equations

s.nonempty = ∃ (x : α), x ∈ s

source

@[simp]

theorem finset.coe_nonempty {α : Type u_1} {s : finset α} :

↑s.nonempty ↔ s.nonempty

source

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

s.nonempty → (∃ (x : α), x ∈ s)

source

theorem finset.nonempty.mono {α : Type u_1} {s t : finset α} :

s ⊆ t → s.nonempty → t.nonempty

source

def finset.empty {α : Type u_1} :

finset α

The empty finset

Equations

finset.empty = {val := 0, nodup := _}

source

@[instance]

def finset.has_emptyc {α : Type u_1} :

has_emptyc (finset α)

Equations

finset.has_emptyc = {emptyc := finset.empty α}

source

@[instance]

def finset.inhabited {α : Type u_1} :

inhabited (finset α)

Equations

finset.inhabited = {default := ∅}

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.ne_empty_of_mem {α : Type u_1} {a : α} {s : finset α} :

a ∈ s → s ≠ ∅

source

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

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 α} :

(∀ (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

theorem finset.nonempty_of_ne_empty {α : Type u_1} {s : finset α} :

s ≠ ∅ → s.nonempty

source

theorem finset.nonempty_iff_ne_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]

theorem finset.coe_empty {α : Type u_1} :

↑∅ = ∅

source

theorem finset.eq_empty_of_not_nonempty {α : Type u_1} (h : ¬nonempty α) (s : finset α) :

s = ∅

A finset for an empty type is empty.

source

@[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

finset.has_singleton = {singleton := λ (a : α), {val := {a}, nodup := _}}

source

@[simp]

theorem finset.singleton_val {α : Type u_1} (a : α) :

{a}.val = a :: 0

source

@[simp]

theorem finset.mem_singleton {α : Type u_1} {a b : α} :

b ∈ {a} ↔ b = a

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

theorem finset.singleton_inj {α : Type u_1} {a b : α} :

{a} = {b} ↔ a = b

source

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

{a}.nonempty

source

@[simp]

theorem finset.singleton_ne_empty {α : Type u_1} (a : α) :

{a} ≠ ∅

source

@[simp]

theorem finset.coe_singleton {α : Type u_1} (a : α) :

↑{a} = {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.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

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

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

finset.cons a s h = {val := a :: s.val, nodup := _}

source

@[simp]

theorem finset.mem_cons {α : Type u_1} {a : α} {s : finset α} {h : a ∉ s} {b : α} :

b ∈ finset.cons a s h ↔ b = a ∨ b ∈ s

source

@[simp]

theorem finset.cons_val {α : Type u_1} {a : α} {s : finset α} (h : a ∉ s) :

(finset.cons a s h).val = a :: s.val

source

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

(∀ (a : α), a ∈ s → a ∉ 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

s.disj_union t h = {val := s.val + t.val, nodup := _}

source

@[simp]

theorem finset.mem_disj_union {α : Type u_1} {s t : finset α} {h : ∀ (a : α), a ∈ s → a ∉ t} {a : α} :

a ∈ s.disj_union t h ↔ a ∈ s ∨ a ∈ t

source

@[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

finset.has_insert = {insert := λ (a : α) (s : finset α), {val := multiset.ndinsert a s.val, nodup := _}}

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).erase_dup

source

theorem finset.insert_val_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∉ s → (has_insert.insert a s).val = a :: s.val

source

@[simp]

theorem finset.mem_insert {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :

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 α] {a b : α} {s : finset α} :

a ∈ s → a ∈ has_insert.insert b s

source

theorem finset.mem_of_mem_insert_of_ne {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :

b ∈ has_insert.insert a s → b ≠ a → b ∈ s

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]

theorem finset.coe_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

↑(has_insert.insert a s) = has_insert.insert a ↑s

source

@[instance]

def finset.is_lawful_singleton {α : Type u_1} [decidable_eq α] :

is_lawful_singleton α (finset α)

Equations

finset.is_lawful_singleton = {insert_emptyc_eq := _}

source

@[simp]

theorem finset.insert_eq_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∈ s → has_insert.insert a s = s

source

@[simp]

theorem finset.insert_singleton_self_eq {α : 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

theorem finset.insert_singleton_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_ne_empty {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

has_insert.insert a s ≠ ∅

source

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

a ∉ s → s ≠ has_insert.insert a t

source

theorem finset.insert_subset {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :

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 α} :

s ⊆ t → has_insert.insert a s ⊆ has_insert.insert a t

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 : α} :

a ∉ s → s ⊂ has_insert.insert a s

source

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

theorem finset.induction_on {α : Type u_1} {p : finset α → Prop} [decidable_eq α] (s : finset α) :

p ∅ → (∀ ⦃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

def finset.subtype_insert_equiv_option {α : Type u_1} [decidable_eq α] {t : finset α} {x : α} :

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

finset.subtype_insert_equiv_option h = {to_fun := λ (y : {i // i ∈ has_insert.insert x t}), dite (↑y = x) (λ (h : ↑y = x), option.none) (λ (h : ¬↑y = x), option.some ⟨↑y, _⟩), inv_fun := λ (y : option {i // i ∈ t}), y.elim ⟨x, _⟩ (λ (z : {i // i ∈ t}), ⟨↑z, _⟩), left_inv := _, right_inv := _}

source

@[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

finset.has_union = {union := λ (s₁ s₂ : finset α), {val := s₁.val.ndunion s₂.val, nodup := _}}

source

theorem finset.union_val_nd {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

(s₁ ∪ s₂).val = s₁.val.ndunion s₂.val

source

@[simp]

theorem finset.union_val {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

(s₁ ∪ s₂).val = s₁.val ∪ s₂.val

source

@[simp]

theorem finset.mem_union {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :

a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

source

@[simp]

theorem finset.disj_union_eq_union {α : Type u_1} [decidable_eq α] (s t : finset α) (h : ∀ (a : α), a ∈ s → a ∉ t) :

s.disj_union t h = s ∪ t

source

theorem finset.mem_union_left {α : Type u_1} [decidable_eq α] {a : α} {s₁ : finset α} (s₂ : finset α) :

a ∈ s₁ → a ∈ s₁ ∪ s₂

source

theorem finset.mem_union_right {α : Type u_1} [decidable_eq α] {a : α} {s₂ : finset α} (s₁ : finset α) :

a ∈ s₂ → a ∈ s₁ ∪ s₂

source

theorem finset.not_mem_union {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :

a ∉ s₁ ∪ s₂ ↔ a ∉ s₁ ∧ a ∉ s₂

source

@[simp]

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₁ s₂ s₃ : finset α} :

s₁ ⊆ s₃ → s₂ ⊆ s₃ → s₁ ∪ s₂ ⊆ s₃

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_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

s₁ ∪ s₂ = s₂ ∪ s₁

source

@[instance]

def finset.is_commutative {α : Type u_1} [decidable_eq α] :

is_commutative (finset α) has_union.union

Equations

finset.is_commutative = _

source

@[simp]

theorem finset.union_assoc {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :

s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

source

@[instance]

def finset.is_associative {α : Type u_1} [decidable_eq α] :

is_associative (finset α) has_union.union

Equations

finset.is_associative = _

source

@[simp]

theorem finset.union_idempotent {α : Type u_1} [decidable_eq α] (s : finset α) :

s ∪ s = s

source

@[instance]

def finset.is_idempotent {α : Type u_1} [decidable_eq α] :

is_idempotent (finset α) has_union.union

Equations

finset.is_idempotent = _

source

theorem finset.union_left_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :

s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)

source

theorem finset.union_right_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :

s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂

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 α} :

t ∪ s = s ↔ t ⊆ s

source

@[simp]

theorem finset.right_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :

s = t ∪ s ↔ t ⊆ s

source

@[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

finset.has_inter = {inter := λ (s₁ s₂ : finset α), {val := s₁.val.ndinter s₂.val, nodup := _}}

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 α} :

a ∈ s₁ ∩ s₂ → a ∈ s₁

source

theorem finset.mem_of_mem_inter_right {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :

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₂ s₃ : finset α} :

s₁ ⊆ s₂ → s₁ ⊆ s₃ → s₁ ⊆ s₂ ∩ s₃

source

@[simp]

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 : α} :

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 : α} :

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 : α} :

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 : α} :

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 α} :

a ∈ s → {a} ∩ s = {a}

source

@[simp]

theorem finset.singleton_inter_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∉ s → {a} ∩ s = ∅

source

@[simp]

theorem finset.inter_singleton_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∈ s → s ∩ {a} = {a}

source

@[simp]

theorem finset.inter_singleton_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∉ s → s ∩ {a} = ∅

source

theorem finset.inter_subset_inter {α : Type u_1} [decidable_eq α] {x y s t : finset α} :

x ⊆ y → s ⊆ t → x ∩ s ⊆ y ∩ t

source

theorem finset.inter_subset_inter_right {α : Type u_1} [decidable_eq α] {x y s : finset α} :

x ⊆ y → x ∩ s ⊆ y ∩ s

source

theorem finset.inter_subset_inter_left {α : Type u_1} [decidable_eq α] {x y s : finset α} :

x ⊆ y → s ∩ x ⊆ s ∩ y

source

@[instance]

def finset.lattice {α : Type u_1} [decidable_eq α] :

lattice (finset α)

Equations

finset.lattice = {sup := has_union.union finset.has_union, le := partial_order.le finset.partial_order, lt := partial_order.lt finset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter finset.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[simp]

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

s ⊔ t = s ∪ t

source

@[simp]

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

s ⊓ t = s ∩ t

source

@[instance]

def finset.semilattice_inf_bot {α : Type u_1} [decidable_eq α] :

semilattice_inf_bot (finset α)

Equations

finset.semilattice_inf_bot = {bot := ∅, le := lattice.le finset.lattice, lt := lattice.lt finset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := lattice.inf finset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def finset.semilattice_sup_bot {α : Type u_1} [decidable_eq α] :

semilattice_sup_bot (finset α)

Equations

finset.semilattice_sup_bot = {bot := semilattice_inf_bot.bot finset.semilattice_inf_bot, le := semilattice_inf_bot.le finset.semilattice_inf_bot, lt := semilattice_inf_bot.lt finset.semilattice_inf_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup finset.lattice, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def finset.distrib_lattice {α : Type u_1} [decidable_eq α] :

distrib_lattice (finset α)

Equations

finset.distrib_lattice = {sup := lattice.sup finset.lattice, le := lattice.le finset.lattice, lt := lattice.lt finset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf finset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

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_eq_empty_iff {α : Type u_1} [decidable_eq α] (A B : finset α) :

A ∪ B = ∅ ↔ A = ∅ ∧ B = ∅

source

def finset.erase {α : Type u_1} [decidable_eq α] :

finset α → α → finset α

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

Equations

s.erase a = {val := s.val.erase a, nodup := _}

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]

theorem finset.erase_empty {α : Type u_1} [decidable_eq α] (a : α) :

∅.erase a = ∅

source

theorem finset.ne_of_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :

b ∈ s.erase a → b ≠ a

source

theorem finset.mem_of_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :

b ∈ s.erase a → b ∈ s

source

theorem finset.mem_erase_of_ne_of_mem {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :

a ≠ b → a ∈ s → a ∈ s.erase b

source

theorem finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :

b ∈ s → b ∉ s.erase a → b = a

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

source

theorem finset.erase_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∉ s → (has_insert.insert a s).erase a = s

source

theorem finset.insert_erase {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

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 α} :

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

@[simp]

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 α} :

a ∈ s → s.erase a ⊂ s

source

theorem finset.erase_eq_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∉ s → s.erase a = s

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

@[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

finset.has_sdiff = {sdiff := λ (s₁ s₂ : finset α), {val := s₁.val - s₂.val, nodup := _}}

source

@[simp]

theorem finset.mem_sdiff {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :

a ∈ s₁ \ s₂ ↔ a ∈ s₁ ∧ a ∉ s₂

source

theorem finset.not_mem_sdiff_of_mem_right {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :

a ∈ t → a ∉ s \ t

source

theorem finset.sdiff_union_of_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} :

s₁ ⊆ s₂ → s₂ \ s₁ ∪ s₁ = s₂

source

theorem finset.union_sdiff_of_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} :

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.inter_sdiff_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

s₁ ∩ (s₂ \ s₁) = ∅

source

@[simp]

theorem finset.sdiff_inter_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

s₂ \ s₁ ∩ s₁ = ∅

source

@[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₁ s₂ s₃ : finset α) :

s₁ \ (s₂ ∩ s₃) = s₁ \ s₂ ∪ s₁ \ s₃

source

@[simp]

theorem finset.sdiff_inter_self_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

s₁ \ (s₁ ∩ s₂) = s₁ \ s₂

source

@[simp]

theorem finset.sdiff_inter_self_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :

s₁ \ (s₂ ∩ s₁) = s₁ \ s₂

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₁ s₂ t₁ t₂ : finset α} :

t₁ ⊆ t₂ → s₂ ⊆ s₁ → t₁ \ s₁ ⊆ t₂ \ s₂

source

theorem finset.sdiff_subset_self {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} :

s₁ \ s₂ ⊆ s₁

source

@[simp]

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_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.sdiff_eq_empty_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :

s \ t = ∅ ↔ 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 : α} :

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 α] (s : finset α) {t : finset α} {x : α} :

x ∈ t → has_insert.insert x s \ t = s \ t

source

@[simp]

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

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.sdiff_sdiff_self_left {α : Type u_1} [decidable_eq α] (s t : finset α) :

s \ (s \ t) = s ∩ t

source

theorem finset.inter_eq_inter_of_sdiff_eq_sdiff {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :

s \ t₁ = s \ t₂ → s ∩ t₁ = s ∩ t₂

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

s.attach = {val := s.val.attach, nodup := _}

source

theorem finset.sizeof_lt_sizeof_of_mem {α : Type u_1} [has_sizeof α] {x : α} {s : finset α} :

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

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

s.piecewise f g = λ (i : α), ite (i ∈ s) (f i) (g i)

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

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 : α} :

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 : α} :

i ∉ s → s.piecewise f g i = g i

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)] :

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

@[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

finset.decidable_dforall_finset = multiset.decidable_dforall_multiset

source

@[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

finset.decidable_eq_pi_finset = multiset.decidable_eq_pi_multiset

source

@[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

finset.decidable_dexists_finset = multiset.decidable_dexists_multiset

source

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

finset α → finset α

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

Equations

finset.filter p s = {val := multiset.filter p s.val, nodup := _}

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.mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} {a : α} :

a ∈ finset.filter p s ↔ a ∈ s ∧ p a

source

@[simp]

theorem finset.filter_subset {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : finset α) :

finset.filter p s ⊆ 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_true {α : Type u_1} {s : finset α} [h : decidable_pred (λ (_x : α), true)] :

finset.filter (λ (_x : α), true) s = s

source

@[simp]

theorem finset.filter_false {α : Type u_1} {h : decidable_pred (λ (a : α), false)} (s : finset α) :

finset.filter (λ (a : α), false) s = ∅

source

@[simp]

theorem finset.filter_true_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :

(∀ (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

theorem finset.filter_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {s : finset α} :

(∀ (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 α} :

s ⊆ t → finset.filter p s ⊆ finset.filter p t

source

@[simp]

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.filter_singleton {α : Type u_1} {p : α → Prop} [decidable_pred p] (a : α) :

finset.filter p {a} = ite (p a) {a} ∅

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} [decidable_eq α] (p q : α → Prop) [decidable_pred p] [decidable_pred q] (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 α} :

finset.filter (λ (i : α), i ∈ t) s = s ∩ 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_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.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

source

theorem finset.filter_inter_filter_neg_eq {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (s : finset α) :

finset.filter p s ∩ finset.filter (λ (a : α), ¬p a) s = ∅

source

theorem finset.subset_union_elim {α : Type u_1} [decidable_eq α] {s : finset α} {t₁ t₂ : set α} :

↑s ⊆ t₁ ∪ t₂ → (∃ (s₁ s₂ : finset α), s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁)

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

@[instance]

def finset.has_sep {α : Type u_1} :

has_sep α (finset α)

The following instance allows us to write { x ∈ s | p x } for finset.filter s p. 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 s p. If p happens to be decidable, the simp-lemma filter_congr_decidable will make sure that finset.filter uses the right instance for decidability.

Equations

finset.has_sep = {sep := λ (p : α → Prop) (x : finset α), finset.filter p x}

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

def finset.range :

ℕ → finset ℕ

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

Equations

finset.range n = {val := multiset.range n, nodup := _}

source

@[simp]

theorem finset.range_coe (n : ℕ) :

(finset.range n).val = multiset.range n

source

@[simp]

theorem finset.mem_range {n m : ℕ} :

m ∈ finset.range n ↔ m < 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.exists_mem_empty_iff {α : Type u_1} (p : α → Prop) :

(∃ (x : α), x ∈ ∅ ∧ p x) ↔ false

source

theorem finset.exists_mem_insert {α : Type u_1} [d : 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} [d : decidable_eq α] (a : α) (s : finset α) (p : α → Prop) :

(∀ (x : α), x ∈ has_insert.insert a s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x

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

not_mem_range_equiv k = {to_fun := λ (i : {n // n ∉ multiset.range k}), i.val - k, inv_fun := λ (j : ℕ), ⟨j + k, _⟩, left_inv := _, right_inv := _}

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, _⟩

source

def option.to_finset {α : Type u_1} :

option α → finset α

Construct an empty or singleton finset from an option

Equations

o.to_finset = option.to_finset._match_1 o
option.to_finset._match_1 (option.some a) = {a}
option.to_finset._match_1 option.none = ∅

source

@[simp]

theorem option.to_finset_none {α : Type u_1} :

option.none.to_finset = ∅

source

@[simp]

theorem option.to_finset_some {α : Type u_1} {a : α} :

(option.some a).to_finset = {a}

source

@[simp]

theorem option.mem_to_finset {α : Type u_1} {a : α} {o : option α} :

a ∈ o.to_finset ↔ a ∈ o

source

def multiset.to_finset {α : Type u_1} [decidable_eq α] :

multiset α → finset α

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

Equations

s.to_finset = {val := s.erase_dup, nodup := _}

source

@[simp]

theorem multiset.to_finset_val {α : Type u_1} [decidable_eq α] (s : multiset α) :

s.to_finset.val = s.erase_dup

source

theorem multiset.to_finset_eq {α : Type u_1} [decidable_eq α] {s : multiset α} (n : s.nodup) :

{val := s, nodup := n} = s.to_finset

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_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 : ℕ) :

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

theorem multiset.to_finset_eq_empty {α : Type u_1} [decidable_eq α] {m : multiset α} :

m.to_finset = ∅ ↔ m = 0

source

def list.to_finset {α : Type u_1} [decidable_eq α] :

list α → finset α

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

Equations

l.to_finset = ↑l.to_finset

source

@[simp]

theorem list.to_finset_val {α : Type u_1} [decidable_eq α] (l : list α) :

l.to_finset.val = ↑(l.erase_dup)

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 α] {a : α} {l : list α} :

a ∈ l.to_finset ↔ 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 α] {a : α} {l : list α} :

(a :: l).to_finset = has_insert.insert a l.to_finset

source

theorem list.to_finset_surjective {α : Type u_1} [decidable_eq α] :

function.surjective list.to_finset

source

def finset.map {α : Type u_1} {β : Type u_2} :

(α ↪ β) → finset α → finset β

When f is an embedding of α in β and s is a finset in α, then s.map f is the image finset in β. The embedding condition guarantees that there are no duplicates in the image.

Equations

finset.map f s = {val := multiset.map ⇑f s.val, nodup := _}

source

@[simp]

theorem finset.map_val {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :

(finset.map f s).val = multiset.map ⇑f s.val

source

@[simp]

theorem finset.map_empty {α : Type u_1} {β : Type u_2} (f : α ↪ β) :

finset.map f ∅ = ∅

source

@[simp]

theorem finset.mem_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} {b : β} :

b ∈ finset.map f s ↔ ∃ (a : α) (H : a ∈ s), ⇑f a = b

source

theorem finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : finset α} :

⇑f a ∈ finset.map f s ↔ a ∈ s

source

theorem finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : finset α} :

a ∈ s → ⇑f a ∈ finset.map f s

source

@[simp]

theorem finset.coe_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :

↑(finset.map f s) = ⇑f '' ↑s

source

theorem finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :

↑(finset.map f s) ⊆ set.range ⇑f

source

theorem finset.map_to_finset {α : Type u_1} {β : Type u_2} {f : α ↪ β} [decidable_eq α] [decidable_eq β] {s : multiset α} :

finset.map f s.to_finset = (multiset.map ⇑f s).to_finset

source

@[simp]

theorem finset.map_refl {α : Type u_1} {s : finset α} :

finset.map (function.embedding.refl α) s = s

source

theorem finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : finset α} {g : β ↪ γ} :

finset.map g (finset.map f s) = finset.map (f.trans g) s

source

theorem finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : finset α} :

finset.map f s₁ ⊆ finset.map f s₂ ↔ s₁ ⊆ s₂

source

theorem finset.map_inj {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : finset α} :

finset.map f s₁ = finset.map f s₂ ↔ s₁ = s₂

source

def finset.map_embedding {α : Type u_1} {β : Type u_2} :

(α ↪ β) → finset α ↪ finset β

Associate to an embedding f from α to β the embedding that maps a finset to its image under f.

Equations

finset.map_embedding f = {to_fun := finset.map f, inj' := _}

source

@[simp]

theorem finset.map_embedding_apply {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} :

⇑(finset.map_embedding f) s = finset.map f s

source

theorem finset.map_filter {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} {p : β → Prop} [decidable_pred p] :

finset.filter p (finset.map f s) = finset.map f (finset.filter (p ∘ ⇑f) s)

source

theorem finset.map_union {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α ↪ β} (s₁ s₂ : finset α) :

finset.map f (s₁ ∪ s₂) = finset.map f s₁ ∪ finset.map f s₂

source

theorem finset.map_inter {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α ↪ β} (s₁ s₂ : finset α) :

finset.map f (s₁ ∩ s₂) = finset.map f s₁ ∩ finset.map f s₂

source

@[simp]

theorem finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) :

finset.map f {a} = {⇑f a}

source

@[simp]

theorem finset.map_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α ↪ β) (a : α) (s : finset α) :

finset.map f (has_insert.insert a s) = has_insert.insert (⇑f a) (finset.map f s)

source

@[simp]

theorem finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} :

finset.map f s = ∅ ↔ s = ∅

source

theorem finset.attach_map_val {α : Type u_1} {s : finset α} :

finset.map (function.embedding.subtype (λ (x : α), x ∈ s)) s.attach = s

source

theorem finset.range_add_one' (n : ℕ) :

finset.range (n + 1) = has_insert.insert 0 (finset.map {to_fun := λ (i : ℕ), i + 1, inj' := _} (finset.range n))

source

def finset.image {α : Type u_1} {β : Type u_2} [decidable_eq β] :

(α → β) → finset α → finset β

image f s is the forward image of s under f.

Equations

finset.image f s = (multiset.map f s.val).to_finset

source

@[simp]

theorem finset.image_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : finset α) :

(finset.image f s).val = (multiset.map f s.val).erase_dup

source

@[simp]

theorem finset.image_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) :

finset.image f ∅ = ∅

source

@[simp]

theorem finset.mem_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} {b : β} :

b ∈ finset.image f s ↔ ∃ (a : α) (H : a ∈ s), f a = b

source

theorem finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) {a : α} {s : finset α} :

a ∈ s → f a ∈ finset.image f s

source

@[simp]

theorem finset.coe_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → β} :

↑(finset.image f s) = f '' ↑s

source

theorem finset.nonempty.image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (f : α → β) :

(finset.image f s).nonempty

source

theorem finset.image_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} [decidable_eq α] {s : multiset α} :

finset.image f s.to_finset = (multiset.map f s).to_finset

source

theorem finset.image_val_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y) → (finset.image f s).val = multiset.map f s.val

source

theorem finset.image_id {α : Type u_1} {s : finset α} [decidable_eq α] :

finset.image id s = s

source

theorem finset.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] {f : α → β} {s : finset α} [decidable_eq γ] {g : β → γ} :

finset.image g (finset.image f s) = finset.image (g ∘ f) s

source

theorem finset.image_subset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s₁ s₂ : finset α} :

s₁ ⊆ s₂ → finset.image f s₁ ⊆ finset.image f s₂

source

theorem finset.image_subset_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : finset β} {f : α → β} :

finset.image f s ⊆ t ↔ ∀ (x : α), x ∈ s → f x ∈ t

source

theorem finset.image_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) :

monotone (finset.image f)

source

theorem finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

↑(finset.image f s) ⊆ set.range f

source

theorem finset.image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} {p : β → Prop} [decidable_pred p] :

finset.filter p (finset.image f s) = finset.image f (finset.filter (p ∘ f) s)

source

theorem finset.image_union {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α → β} (s₁ s₂ : finset α) :

finset.image f (s₁ ∪ s₂) = finset.image f s₁ ∪ finset.image f s₂

source

theorem finset.image_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} [decidable_eq α] (s₁ s₂ : finset α) :

(∀ (x y : α), f x = f y → x = y) → finset.image f (s₁ ∩ s₂) = finset.image f s₁ ∩ finset.image f s₂

source

@[simp]

theorem finset.image_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (a : α) :

finset.image f {a} = {f a}

source

@[simp]

theorem finset.image_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α → β) (a : α) (s : finset α) :

finset.image f (has_insert.insert a s) = has_insert.insert (f a) (finset.image f s)

source

@[simp]

theorem finset.image_eq_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

finset.image f s = ∅ ↔ s = ∅

source

theorem finset.attach_image_val {α : Type u_1} [decidable_eq α] {s : finset α} :

finset.image subtype.val s.attach = s

source

@[simp]

theorem finset.attach_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

(has_insert.insert a s).attach = has_insert.insert ⟨a, _⟩ (finset.image (λ (x : {x // x ∈ s}), ⟨x.val, _⟩) s.attach)

source

theorem finset.map_eq_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α ↪ β) (s : finset α) :

finset.map f s = finset.image ⇑f s

source

theorem finset.image_const {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (b : β) :

finset.image (λ (a : α), b) s = {b}

source

@[instance]

def finset.functor [Π (P : Prop), decidable P] :

functor finset

Because finset.image requires a decidable_eq instances for the target type, we can only construct a functor finset when working classically.

Equations

finset.functor = {map := λ (α β : Type u_1) (f : α → β) (s : finset α), finset.image f s, map_const := λ (α β : Type u_1), (λ (f : β → α) (s : finset β), finset.image f s) ∘ function.const β}

source

@[instance]

def finset.is_lawful_functor [Π (P : Prop), decidable P] :

is_lawful_functor finset

Equations

finset.is_lawful_functor = _

source

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

finset α → finset (subtype p)

Given a finset s and a predicate p, s.subtype p is the finset of subtype p whose elements belong to s.

Equations

finset.subtype p s = finset.map {to_fun := λ (x : {x // x ∈ finset.filter p s}), ⟨x.val, _⟩, inj' := _} (finset.filter p s).attach

source

@[simp]

theorem finset.mem_subtype {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} {a : subtype p} :

a ∈ finset.subtype p s ↔ a.val ∈ s

source

@[simp]

theorem finset.subtype_map {α : Type u_1} {s : finset α} (p : α → Prop) [decidable_pred p] :

finset.map (function.embedding.subtype p) (finset.subtype p s) = finset.filter p s

s.subtype p converts back to s.filter p with embedding.subtype.

source

theorem finset.subtype_map_of_mem {α : Type u_1} {s : finset α} {p : α → Prop} [decidable_pred p] :

(∀ (x : α), x ∈ s → p x) → finset.map (function.embedding.subtype p) (finset.subtype p s) = s

If all elements of a finset satisfy the predicate p, s.subtype p converts back to s with embedding.subtype.

source

theorem finset.property_of_mem_map_subtype {α : Type u_1} {p : α → Prop} (s : finset {x // p x}) {a : α} :

a ∈ finset.map (function.embedding.subtype (λ (x : α), p x)) s → p a

If a finset of a subtype is converted to the main type with embedding.subtype, all elements of the result have the property of the subtype.

source

theorem finset.not_mem_map_subtype_of_not_property {α : Type u_1} {p : α → Prop} (s : finset {x // p x}) {a : α} :

¬p a → a ∉ finset.map (function.embedding.subtype (λ (x : α), p x)) s

If a finset of a subtype is converted to the main type with embedding.subtype, the result does not contain any value that does not satisfy the property of the subtype.

source

theorem finset.map_subtype_subset {α : Type u_1} {t : set α} (s : finset ↥t) :

↑(finset.map (function.embedding.subtype (λ (x : α), x ∈ t)) s) ⊆ t

If a finset of a subtype is converted to the main type with embedding.subtype, the result is a subset of the set giving the subtype.

source

theorem finset.subset_image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset β} {t : set α} :

↑s ⊆ f '' t ↔ ∃ (s' : finset α), ↑s' ⊆ t ∧ finset.image f s' = s

source

theorem multiset.to_finset_map {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (m : multiset α) :

(multiset.map f m).to_finset = finset.image f m.to_finset

source

def finset.card {α : Type u_1} :

finset α → ℕ

card s is the cardinality (number of elements) of s.

Equations

s.card = s.val.card

source

theorem finset.card_def {α : Type u_1} (s : finset α) :

s.card = s.val.card

source

@[simp]

theorem finset.card_mk {α : Type u_1} {m : multiset α} {nodup : m.nodup} :

{val := m, nodup := nodup}.card = m.card

source

@[simp]

theorem finset.card_empty {α : Type u_1} :

∅.card = 0

source

@[simp]

theorem finset.card_eq_zero {α : Type u_1} {s : finset α} :

s.card = 0 ↔ s = ∅

source

theorem finset.card_pos {α : Type u_1} {s : finset α} :

0 < s.card ↔ s.nonempty

source

theorem finset.card_ne_zero_of_mem {α : Type u_1} {s : finset α} {a : α} :

a ∈ s → s.card ≠ 0

source

theorem finset.card_eq_one {α : Type u_1} {s : finset α} :

s.card = 1 ↔ ∃ (a : α), s = {a}

source

@[simp]

theorem finset.card_insert_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∉ s → (has_insert.insert a s).card = s.card + 1

source

theorem finset.card_insert_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∈ s → (has_insert.insert a s).card = s.card

source

theorem finset.card_insert_le {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

(has_insert.insert a s).card ≤ s.card + 1

source

@[simp]

theorem finset.card_singleton {α : Type u_1} (a : α) :

{a}.card = 1

source

theorem finset.card_singleton_inter {α : Type u_1} [decidable_eq α] {x : α} {s : finset α} :

({x} ∩ s).card ≤ 1

source

theorem finset.card_erase_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∈ s → (s.erase a).card = s.card.pred

source

theorem finset.card_erase_lt_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

a ∈ s → (s.erase a).card < s.card

source

theorem finset.card_erase_le {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :

(s.erase a).card ≤ s.card

source

@[simp]

theorem finset.card_range (n : ℕ) :

(finset.range n).card = n

source

@[simp]

theorem finset.card_attach {α : Type u_1} {s : finset α} :

s.attach.card = s.card

source

theorem multiset.to_finset_card_le {α : Type u_1} [decidable_eq α] (m : multiset α) :

m.to_finset.card ≤ m.card

source

theorem list.to_finset_card_le {α : Type u_1} [decidable_eq α] (l : list α) :

l.to_finset.card ≤ l.length

source

theorem finset.card_image_le {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

(finset.image f s).card ≤ s.card

source

theorem finset.card_image_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y) → (finset.image f s).card = s.card

source

theorem finset.card_image_of_injective {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} (s : finset α) :

function.injective f → (finset.image f s).card = s.card

source

@[simp]

theorem finset.card_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) {s : finset α} :

(finset.map f s).card = s.card

source

theorem finset.card_eq_of_bijective {α : Type u_1} {s : finset α} {n : ℕ} (f : Π (i : ℕ), i < n → α) :

(∀ (a : α), a ∈ s → (∃ (i : ℕ) (h : i < n), f i h = a)) → (∀ (i : ℕ) (h : i < n), f i h ∈ s) → (∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) → s.card = n

source

theorem finset.card_eq_succ {α : Type u_1} [decidable_eq α] {s : finset α} {n : ℕ} :

s.card = n + 1 ↔ ∃ (a : α) (t : finset α), a ∉ t ∧ has_insert.insert a t = s ∧ t.card = n

source

theorem finset.card_le_of_subset {α : Type u_1} {s t : finset α} :

s ⊆ t → s.card ≤ t.card

source

theorem finset.eq_of_subset_of_card_le {α : Type u_1} {s t : finset α} :

s ⊆ t → t.card ≤ s.card → s = t

source

theorem finset.card_lt_card {α : Type u_1} {s t : finset α} :

s ⊂ t → s.card < t.card

source

theorem finset.card_le_card_of_inj_on {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : α → β) :

(∀ (a : α), a ∈ s → f a ∈ t) → (∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂) → s.card ≤ t.card

source

theorem finset.card_le_of_inj_on {α : Type u_1} {n : ℕ} {s : finset α} (f : ℕ → α) :

(∀ (i : ℕ), i < n → f i ∈ s) → (∀ (i j : ℕ), i < n → j < n → f i = f j → i = j) → n ≤ s.card

source

def finset.strong_induction_on {α : Type u_1} {p : finset α → Sort u_2} (s : finset α) :

(Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s) → p s

Suppose that, given objects defined on all strict subsets of any finset s, one knows how to define an object on s. Then one can inductively define an object on all finsets, starting from the empty set and iterating. This can be used either to define data, or to prove properties.

Equations

{val := s, nodup := nd}.strong_induction_on ih = s.strong_induction_on (λ (s : multiset α) (IH : Π (t : multiset α), t < s → Π (_a : t.nodup), p {val := t, nodup := _a}) (nd : s.nodup), ih {val := s, nodup := nd} (λ (_x : finset α), finset.strong_induction_on._match_1 s IH nd _x)) nd
finset.strong_induction_on._match_1 s IH nd {val := t, nodup := nd'} = λ (ss : {val := t, nodup := nd'} ⊂ {val := s, nodup := nd}), IH t _ nd'

source

theorem finset.case_strong_induction_on {α : Type u_1} [decidable_eq α] {p : finset α → Prop} (s : finset α) :

p ∅ → (∀ (a : α) (s : finset α), a ∉ s → (∀ (t : finset α), t ⊆ s → p t) → p (has_insert.insert a s)) → p s

source

theorem finset.card_congr {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a ∈ s → β) :

(∀ (a : α) (ha : a ∈ s), f a ha ∈ t) → (∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b) → (∀ (b : β), b ∈ t → (∃ (a : α) (ha : a ∈ s), f a ha = b)) → s.card = t.card

source

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

(s ∪ t).card + (s ∩ t).card = s.card + t.card

source

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

(s ∪ t).card ≤ s.card + t.card

source

theorem finset.card_union_eq {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t → (s ∪ t).card = s.card + t.card

source

theorem finset.surj_on_of_inj_on_of_card_le {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a ∈ s → β) (hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t) (hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) (hst : t.card ≤ s.card) (b : β) :

b ∈ t → (∃ (a : α) (ha : a ∈ s), b = f a ha)

source

theorem finset.inj_on_of_surj_on_of_card_le {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a ∈ s → β) (hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t) (hsurj : ∀ (b : β), b ∈ t → (∃ (a : α) (ha : a ∈ s), b = f a ha)) (hst : s.card ≤ t.card) ⦃a₁ a₂ : α⦄ (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s) :

f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂

source

def finset.bind {α : Type u_1} {β : Type u_2} [decidable_eq β] :

finset α → (α → finset β) → finset β

bind s t is the union of t x over x ∈ s

Equations

s.bind t = (s.val.bind (λ (a : α), (t a).val)).to_finset

source

@[simp]

theorem finset.bind_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (t : α → finset β) :

(s.bind t).val = (s.val.bind (λ (a : α), (t a).val)).erase_dup

source

@[simp]

theorem finset.bind_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {t : α → finset β} :

∅.bind t = ∅

source

@[simp]

theorem finset.mem_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} {b : β} :

b ∈ s.bind t ↔ ∃ (a : α) (H : a ∈ s), b ∈ t a

source

@[simp]

theorem finset.bind_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} [decidable_eq α] {a : α} :

(has_insert.insert a s).bind t = t a ∪ s.bind t

source

@[simp]

theorem finset.singleton_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] {t : α → finset β} {a : α} :

{a}.bind t = t a

source

theorem finset.bind_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → finset β) (t : finset β) :

s.bind f ∩ t = s.bind (λ (x : α), f x ∩ t)

source

theorem finset.inter_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] (t : finset β) (s : finset α) (f : α → finset β) :

t ∩ s.bind f = s.bind (λ (x : α), t ∩ f x)

source

theorem finset.image_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] {f : α → β} {s : finset α} {t : β → finset γ} :

(finset.image f s).bind t = s.bind (λ (a : α), t (f a))

source

theorem finset.bind_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] {s : finset α} {t : α → finset β} {f : β → γ} :

finset.image f (s.bind t) = s.bind (λ (a : α), finset.image f (t a))

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.bind (λ (a : α), (t a).to_finset)

source

theorem finset.bind_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t₁ t₂ : α → finset β} :

(∀ (a : α), a ∈ s → t₁ a ⊆ t₂ a) → s.bind t₁ ⊆ s.bind t₂

source

theorem finset.bind_subset_bind_of_subset_left {β : Type u_2} [decidable_eq β] {α : Type u_1} {s₁ s₂ : finset α} (t : α → finset β) :

s₁ ⊆ s₂ → s₁.bind t ⊆ s₂.bind t

source

theorem finset.bind_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → β} :

s.bind (λ (a : α), {f a}) = finset.image f s

source

@[simp]

theorem finset.bind_singleton_eq_self {α : Type u_1} {s : finset α} [decidable_eq α] :

s.bind has_singleton.singleton = s

source

theorem finset.image_bind_filter_eq {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (s : finset β) (g : β → α) :

(finset.image g s).bind (λ (a : α), finset.filter (λ (c : β), g c = a) s) = s

source

def finset.product {α : Type u_1} {β : Type u_2} :

finset α → finset β → finset (α × β)

product s t is the set of pairs (a, b) such that a ∈ s and b ∈ t.

Equations

s.product t = {val := s.val.product t.val, nodup := _}

source

@[simp]

theorem finset.product_val {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :

(s.product t).val = s.val.product t.val

source

@[simp]

theorem finset.mem_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {p : α × β} :

p ∈ s.product t ↔ p.fst ∈ s ∧ p.snd ∈ t

source

theorem finset.subset_product {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {s : finset (α × β)} :

s ⊆ (finset.image prod.fst s).product (finset.image prod.snd s)

source

theorem finset.product_eq_bind {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :

s.product t = s.bind (λ (a : α), finset.image (λ (b : β), (a, b)) t)

source

@[simp]

theorem finset.card_product {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :

(s.product t).card = s.card * t.card

source

def finset.sigma {α : Type u_1} {σ : α → Type u_4} :

finset α → (Π (a : α), finset (σ a)) → finset (Σ (a : α), σ a)

sigma s t is the set of dependent pairs ⟨a, b⟩ such that a ∈ s and b ∈ t a.

Equations

s.sigma t = {val := s.val.sigma (λ (a : α), (t a).val), nodup := _}

source

@[simp]

theorem finset.mem_sigma {α : Type u_1} {σ : α → Type u_4} {s : finset α} {t : Π (a : α), finset (σ a)} {p : sigma σ} :

p ∈ s.sigma t ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst

source

theorem finset.sigma_mono {α : Type u_1} {σ : α → Type u_4} {s₁ s₂ : finset α} {t₁ t₂ : Π (a : α), finset (σ a)} :

s₁ ⊆ s₂ → (∀ (a : α), t₁ a ⊆ t₂ a) → s₁.sigma t₁ ⊆ s₂.sigma t₂

source

theorem finset.sigma_eq_bind {α : Type u_1} {σ : α → Type u_4} [decidable_eq (Σ (a : α), σ a)] (s : finset α) (t : Π (a : α), finset (σ a)) :

s.sigma t = s.bind (λ (a : α), finset.map (function.embedding.sigma_mk a) (t a))

source

theorem finset.disjoint_left {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t

source

theorem finset.disjoint_val {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t ↔ s.val.disjoint t.val

source

theorem finset.disjoint_iff_inter_eq_empty {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t ↔ s ∩ t = ∅

source

@[instance]

def finset.decidable_disjoint {α : Type u_1} [decidable_eq α] (U V : finset α) :

decidable (disjoint U V)

Equations

U.decidable_disjoint V = decidable_of_decidable_of_iff (finset.has_decidable_eq (U ⊓ V) ⊥) _

source

theorem finset.disjoint_right {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t ↔ ∀ {a : α}, a ∈ t → a ∉ s

source

theorem finset.disjoint_iff_ne {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b

source

theorem finset.disjoint_of_subset_left {α : Type u_1} [decidable_eq α] {s t u : finset α} :

s ⊆ u → disjoint u t → disjoint s t

source

theorem finset.disjoint_of_subset_right {α : Type u_1} [decidable_eq α] {s t u : finset α} :

t ⊆ u → disjoint s u → disjoint s t

source

@[simp]

theorem finset.disjoint_empty_left {α : Type u_1} [decidable_eq α] (s : finset α) :

disjoint ∅ s

source

@[simp]

theorem finset.disjoint_empty_right {α : Type u_1} [decidable_eq α] (s : finset α) :

disjoint s ∅

source

@[simp]

theorem finset.singleton_disjoint {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :

disjoint {a} s ↔ a ∉ s

source

@[simp]

theorem finset.disjoint_singleton {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :

disjoint s {a} ↔ a ∉ s

source

@[simp]

theorem finset.disjoint_insert_left {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :

disjoint (has_insert.insert a s) t ↔ a ∉ t ∧ disjoint s t

source

@[simp]

theorem finset.disjoint_insert_right {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :

disjoint s (has_insert.insert a t) ↔ a ∉ s ∧ disjoint s t

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.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 α} :

disjoint s t → s \ t = s

source

theorem finset.disjoint_self_iff_empty {α : Type u_1} [decidable_eq α] (s : finset α) :

disjoint s s ↔ s = ∅

source

theorem finset.disjoint_bind_left {α : Type u_1} [decidable_eq α] {ι : Type u_2} (s : finset ι) (f : ι → finset α) (t : finset α) :

disjoint (s.bind f) t ↔ ∀ (i : ι), i ∈ s → disjoint (f i) t

source

theorem finset.disjoint_bind_right {α : Type u_1} [decidable_eq α] {ι : Type u_2} (s : finset α) (t : finset ι) (f : ι → finset α) :

disjoint s (t.bind f) ↔ ∀ (i : ι), i ∈ t → disjoint s (f i)

source

@[simp]

theorem finset.card_disjoint_union {α : Type u_1} [decidable_eq α] {s t : finset α} :

disjoint s t → (s ∪ t).card = s.card + t.card

source

theorem finset.card_sdiff {α : Type u_1} [decidable_eq α] {s t : finset α} :

s ⊆ t → (t \ s).card = t.card - s.card

source

theorem finset.disjoint_filter {α : Type u_1} [decidable_eq α] {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} [decidable_eq α] {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_iff_disjoint_coe {α : Type u_1} {a b : finset α} [decidable_eq α] :

disjoint a b ↔ disjoint ↑a ↑b

source

theorem finset.exists_intermediate_set {α : Type u_1} {A B : finset α} (i : ℕ) :

i + B.card ≤ A.card → B ⊆ A → (∃ (C : finset α), B ⊆ C ∧ C ⊆ A ∧ C.card = i + B.card)

Given a set A and a set B inside it, we can shrink A to any appropriate size, and keep B inside it.

source

theorem finset.exists_smaller_set {α : Type u_1} (A : finset α) (i : ℕ) :

i ≤ A.card → (∃ (B : finset α), B ⊆ A ∧ B.card = i)

We can shrink A to any smaller size.

source

def finset.fin_range (k : ℕ) :

finset (fin k)

finset.fin_range k is the finset {0, 1, ..., k-1}, as a finset (fin k).

Equations

finset.fin_range k = {val := ↑(list.fin_range k), nodup := _}

source

@[simp]

theorem finset.fin_range_card {k : ℕ} :

(finset.fin_range k).card = k

source

@[simp]

theorem finset.mem_fin_range {k : ℕ} (m : fin k) :

m ∈ finset.fin_range k

source

def finset.attach_fin (s : finset ℕ) {n : ℕ} :

(∀ (m : ℕ), m ∈ s → m < n) → finset (fin n)

Given a finset s of ℕ contained in {0,..., n-1}, the corresponding finset in fin n is s.attach_fin h where h is a proof that all elements of s are less than n.

Equations

s.attach_fin h = {val := multiset.pmap (λ (a : ℕ) (ha : a < n), ⟨a, ha⟩) s.val h, nodup := _}

source

@[simp]

theorem finset.mem_attach_fin {n : ℕ} {s : finset ℕ} (h : ∀ (m : ℕ), m ∈ s → m < n) {a : fin n} :

a ∈ s.attach_fin h ↔ a.val ∈ s

source

@[simp]

theorem finset.card_attach_fin {n : ℕ} (s : finset ℕ) (h : ∀ (m : ℕ), m ∈ s → m < n) :

(s.attach_fin h).card = s.card

source

def finset.choose_x {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : finset α) :

(∃! (a : α), a ∈ l ∧ p a) → {a // a ∈ l ∧ p a}

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

Equations

finset.choose_x p l hp = multiset.choose_x p l.val hp

source

def finset.choose {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : finset α) :

(∃! (a : α), a ∈ l ∧ p a) → α

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

Equations

finset.choose p l hp = ↑(finset.choose_x p l hp)

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.lt_wf {α : Type u_1} :

well_founded has_lt.lt

source

theorem list.to_finset_card_of_nodup {α : Type u_1} [decidable_eq α] {l : list α} :

l.nodup → l.to_finset.card = l.length

mathlib documentation

data.finset.basic

Finite sets

set coercion

extensionality

subset

Nonempty

empty

singleton

cons

disjoint union

insert

union

inter

lattice laws

erase

sdiff

attach

piecewise

filter

range

erase_dup on list and multiset

map

image

card

bind

prod

sigma

disjoint

choose

General documentation

Additional documentation

Library

mathlib documentation

data.​finset.​basic

Finite sets

set coercion

extensionality

subset

Nonempty

empty

singleton

cons

disjoint union

insert

union

inter

lattice laws

erase

sdiff

attach

piecewise

filter

range

erase_dup on list and multiset

map

image

card

bind

prod

sigma

disjoint

choose

General documentation

Additional documentation

Library

data.finset.basic