mathlib3 documentation

data.finset.card

Cardinality of a finite set #

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

This defines the cardinality of a finset and provides induction principles for finsets.

Main declarations #

Induction principles #

TODO #

Should we add a noncomputable version?

source
def finset.card {α : Type u_1} (s : finset α) :
ℕ

s.card is the number of elements of s, aka its cardinality.

Equations
source
theorem finset.card_def {α : Type u_1} (s : finset α) :
s.card = ⇑multiset.card s.val
source
@[simp]
theorem finset.card_mk {α : Type u_1} {m : multiset α} {nodup : m.nodup} :
{val := m, nodup := nodup}.card = ⇑multiset.card m
source
@[simp]
theorem finset.card_empty {α : Type u_1} :
∅.card = 0
source
theorem finset.card_le_of_subset {α : Type u_1} {s t : finset α} :
s ⊆ t → s.card ≤ t.card
source
theorem finset.card_mono {α : Type u_1} :
monotone finset.card
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.nonempty.card_pos {α : Type u_1} {s : finset α} :
s.nonempty → 0 < s.card

Alias of the reverse direction of finset.card_pos.

source
theorem finset.card_ne_zero_of_mem {α : Type u_1} {s : finset α} {a : α} (h : a ∈ s) :
s.card ≠ 0
source
@[simp]
theorem finset.card_singleton {α : Type u_1} (a : α) :
{a}.card = 1
source
theorem finset.card_singleton_inter {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
({a} ∩ s).card ≤ 1
source
@[simp]
theorem finset.card_cons {α : Type u_1} {s : finset α} {a : α} (h : a ∉ s) :
(finset.cons a s h).card = s.card + 1
source
@[simp]
theorem finset.card_insert_of_not_mem {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] (h : a ∉ s) :
(has_insert.insert a s).card = s.card + 1
source
theorem finset.card_insert_of_mem {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] (h : 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
theorem finset.card_insert_eq_ite {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
(has_insert.insert a s).card = ite (a ∈ s) s.card (s.card + 1)

If a ∈ s is known, see also finset.card_insert_of_mem and finset.card_insert_of_not_mem.

source
@[simp]
theorem finset.card_doubleton {α : Type u_1} {a b : α} [decidable_eq α] (h : a ≠ b) :
{a, b}.card = 2
source
@[simp]
theorem finset.card_erase_of_mem {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
a ∈ s → (s.erase a).card = s.card - 1
source
@[simp]
theorem finset.card_erase_add_one {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
a ∈ s → (s.erase a).card + 1 = s.card
source
theorem finset.card_erase_lt_of_mem {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
a ∈ s → (s.erase a).card < s.card
source
theorem finset.card_erase_le {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
(s.erase a).card ≤ s.card
source
theorem finset.pred_card_le_card_erase {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
s.card - 1 ≤ (s.erase a).card
source
theorem finset.card_erase_eq_ite {α : Type u_1} {s : finset α} {a : α} [decidable_eq α] :
(s.erase a).card = ite (a ∈ s) (s.card - 1) s.card

If a ∈ s is known, see also finset.card_erase_of_mem and finset.erase_eq_of_not_mem.

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.card_to_finset {α : Type u_1} [decidable_eq α] (m : multiset α) :
m.to_finset.card = ⇑multiset.card m.dedup
source
theorem multiset.to_finset_card_le {α : Type u_1} [decidable_eq α] (m : multiset α) :
m.to_finset.card ≤ ⇑multiset.card m
source
theorem multiset.to_finset_card_of_nodup {α : Type u_1} [decidable_eq α] {m : multiset α} (h : m.nodup) :
m.to_finset.card = ⇑multiset.card m
source
theorem list.card_to_finset {α : Type u_1} [decidable_eq α] (l : list α) :
l.to_finset.card = l.dedup.length
source
theorem list.to_finset_card_le {α : Type u_1} [decidable_eq α] (l : list α) :
l.to_finset.card ≤ l.length
source
theorem list.to_finset_card_of_nodup {α : Type u_1} [decidable_eq α] {l : list α} (h : l.nodup) :
l.to_finset.card = l.length
source
@[simp]
theorem finset.length_to_list {α : Type u_1} (s : finset α) :
s.to_list.length = s.card
source
theorem finset.card_image_le {α : Type u_1} {β : Type u_2} {s : finset α} {f : α → β} [decidable_eq β] :
(finset.image f s).card ≤ s.card
source
theorem finset.card_image_of_inj_on {α : Type u_1} {β : Type u_2} {s : finset α} {f : α → β} [decidable_eq β] (H : set.inj_on f ↑s) :
(finset.image f s).card = s.card
source
theorem finset.inj_on_of_card_image_eq {α : Type u_1} {β : Type u_2} {s : finset α} {f : α → β} [decidable_eq β] (H : (finset.image f s).card = s.card) :
set.inj_on f ↑s
source
theorem finset.card_image_iff {α : Type u_1} {β : Type u_2} {s : finset α} {f : α → β} [decidable_eq β] :
(finset.image f s).card = s.card ↔ set.inj_on f ↑s
source
theorem finset.card_image_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} [decidable_eq β] (s : finset α) (H : function.injective f) :
(finset.image f s).card = s.card
source
theorem finset.fiber_card_ne_zero_iff_mem_image {α : Type u_1} {β : Type u_2} (s : finset α) (f : α → β) [decidable_eq β] (y : β) :
(finset.filter (λ (x : α), f x = y) s).card ≠ 0 ↔ y ∈ finset.image f s
source
@[simp]
theorem finset.card_map {α : Type u_1} {β : Type u_2} {s : finset α} (f : α ↪ β) :
(finset.map f s).card = s.card
source
@[simp]
theorem finset.card_subtype {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) :
(finset.subtype p s).card = (finset.filter p s).card
source
theorem finset.card_filter_le {α : Type u_1} (s : finset α) (p : α → Prop) [decidable_pred p] :
(finset.filter p s).card ≤ s.card
source
theorem finset.eq_of_subset_of_card_le {α : Type u_1} {s t : finset α} (h : s ⊆ t) (h₂ : t.card ≤ s.card) :
s = t
source
theorem finset.eq_of_superset_of_card_ge {α : Type u_1} {s t : finset α} (hst : s ⊆ t) (hts : t.card ≤ s.card) :
t = s
source
theorem finset.subset_iff_eq_of_card_le {α : Type u_1} {s t : finset α} (h : t.card ≤ s.card) :
s ⊆ t ↔ s = t
source
theorem finset.map_eq_of_subset {α : Type u_1} {s : finset α} {f : α ↪ α} (hs : finset.map f s ⊆ s) :
finset.map f s = s
source
theorem finset.filter_card_eq {α : Type u_1} {s : finset α} {p : α → Prop} [decidable_pred p] (h : (finset.filter p s).card = s.card) (x : α) (hx : x ∈ s) :
p x
source
theorem finset.card_lt_card {α : Type u_1} {s t : finset α} (h : s ⊂ t) :
s.card < t.card
source
theorem finset.card_eq_of_bijective {α : Type u_1} {s : finset α} {n : ℕ} (f : Π (i : ℕ), i < n → α) (hf : ∀ (a : α), a ∈ s → (∃ (i : ℕ) (h : i < n), f i h = a)) (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s) (f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) :
s.card = n
source
theorem finset.card_congr {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a ∈ s → β) (h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t) (h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b) (h₃ : ∀ (b : β), b ∈ t → (∃ (a : α) (ha : a ∈ s), f a ha = b)) :
s.card = t.card
source
theorem finset.card_le_card_of_inj_on {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : α → β) (hf : ∀ (a : α), a ∈ s → f a ∈ t) (f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂) :
s.card ≤ t.card
source
theorem finset.exists_ne_map_eq_of_card_lt_of_maps_to {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (hc : t.card < s.card) {f : α → β} (hf : ∀ (a : α), a ∈ s → f a ∈ t) :
∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x ≠ y ∧ f x = f y

If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.

source
theorem finset.le_card_of_inj_on_range {α : Type u_1} {s : finset α} {n : ℕ} (f : ℕ → α) (hf : ∀ (i : ℕ), i < n → f i ∈ s) (f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j) :
n ≤ s.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 : β) (H : 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) (ha₁a₂ : f a₁ ha₁ = f a₂ ha₂) :
a₁ = a₂
source
@[simp]
theorem finset.card_disj_union {α : Type u_1} (s t : finset α) (h : disjoint s t) :
(s.disj_union t h).card = s.card + t.card

Lattice structure #

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_inter_add_card_union {α : 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} {s t : finset α} [decidable_eq α] (h : disjoint s t) :
(s ∪ t).card = s.card + t.card
source
@[simp]
theorem finset.card_disjoint_union {α : Type u_1} {s t : finset α} [decidable_eq α] (h : disjoint s t) :
(s ∪ t).card = s.card + t.card
source
theorem finset.card_sdiff {α : Type u_1} {s t : finset α} [decidable_eq α] (h : s ⊆ t) :
(t \ s).card = t.card - s.card
source
theorem finset.card_sdiff_add_card_eq_card {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :
(t \ s).card + s.card = t.card
source
theorem finset.le_card_sdiff {α : Type u_1} [decidable_eq α] (s t : finset α) :
t.card - s.card ≤ (t \ s).card
source
theorem finset.card_le_card_sdiff_add_card {α : Type u_1} {s t : finset α} [decidable_eq α] :
s.card ≤ (s \ t).card + t.card
source
theorem finset.card_sdiff_add_card {α : Type u_1} {s t : finset α} [decidable_eq α] :
(s \ t).card + t.card = (s ∪ t).card
source
theorem finset.filter_card_add_filter_neg_card_eq_card {α : Type u_1} {s : finset α} (p : α → Prop) [decidable_pred p] :
(finset.filter p s).card + (finset.filter (not ∘ p) s).card = s.card
source
theorem finset.exists_intermediate_set {α : Type u_1} {A B : finset α} (i : ℕ) (h₁ : i + B.card ≤ A.card) (h₂ : 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 : ℕ) (h₁ : i ≤ A.card) :
∃ (B : finset α), B ⊆ A ∧ B.card = i

We can shrink A to any smaller size.

source
theorem finset.exists_subset_or_subset_of_two_mul_lt_card {α : Type u_1} [decidable_eq α] {X Y : finset α} {n : ℕ} (hXY : 2 * n < (X ∪ Y).card) :
∃ (C : finset α), n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)

Explicit description of a finset from its card #

source
theorem finset.card_eq_one {α : Type u_1} {s : finset α} :
s.card = 1 ↔ ∃ (a : α), s = {a}
source
theorem finset.exists_eq_insert_iff {α : Type u_1} [decidable_eq α] {s t : finset α} :
(∃ (a : α) (H : a ∉ s), has_insert.insert a s = t) ↔ s ⊆ t ∧ s.card + 1 = t.card
source
theorem finset.card_le_one {α : Type u_1} {s : finset α} :
s.card ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
source
theorem finset.card_le_one_iff {α : Type u_1} {s : finset α} :
s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
source
theorem finset.card_le_one_iff_subset_singleton {α : Type u_1} {s : finset α} [nonempty α] :
s.card ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
source
theorem finset.card_le_one_of_subsingleton {α : Type u_1} [subsingleton α] (s : finset α) :
s.card ≤ 1

A finset of a subsingleton type has cardinality at most one.

source
theorem finset.one_lt_card {α : Type u_1} {s : finset α} :
1 < s.card ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ s), a ≠ b
source
theorem finset.one_lt_card_iff {α : Type u_1} {s : finset α} :
1 < s.card ↔ ∃ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
source
theorem finset.two_lt_card_iff {α : Type u_1} {s : finset α} :
2 < s.card ↔ ∃ (a b c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
source
theorem finset.two_lt_card {α : Type u_1} {s : finset α} :
2 < s.card ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ s) (c : α) (H : c ∈ s), a ≠ b ∧ a ≠ c ∧ b ≠ c
source
theorem finset.exists_ne_of_one_lt_card {α : Type u_1} {s : finset α} (hs : 1 < s.card) (a : α) :
∃ (b : α), b ∈ s ∧ b ≠ a
source
theorem finset.card_eq_succ {α : Type u_1} {s : finset α} {n : ℕ} [decidable_eq α] :
s.card = n + 1 ↔ ∃ (a : α) (t : finset α), a ∉ t ∧ has_insert.insert a t = s ∧ t.card = n
source
theorem finset.card_eq_two {α : Type u_1} {s : finset α} [decidable_eq α] :
s.card = 2 ↔ ∃ (x y : α), x ≠ y ∧ s = {x, y}
source
theorem finset.card_eq_three {α : Type u_1} {s : finset α} [decidable_eq α] :
s.card = 3 ↔ ∃ (x y z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Inductions #

source
def finset.strong_induction {α : Type u_1} {p : finset α → Sort u_2} (H : Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s) (s : finset α) :
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
source
theorem finset.strong_induction_eq {α : Type u_1} {p : finset α → Sort u_2} (H : Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s) (s : finset α) :
finset.strong_induction H s = H s (λ (t : finset α) (h : t ⊂ s), finset.strong_induction H t)
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

Analogue of strong_induction with order of arguments swapped.

Equations
source
theorem finset.strong_induction_on_eq {α : Type u_1} {p : finset α → Sort u_2} (s : finset α) (H : Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s) :
s.strong_induction_on H = H s (λ (t : finset α) (h : t ⊂ s), t.strong_induction_on H)
source
theorem finset.case_strong_induction_on {α : Type u_1} [decidable_eq α] {p : finset α → Prop} (s : finset α) (h₀ : p ∅) (h₁ : ∀ (a : α) (s : finset α), a ∉ s → (∀ (t : finset α), t ⊆ s → p t) → p (has_insert.insert a s)) :
p s
source
def finset.strong_downward_induction {α : Type u_1} {p : finset α → Sort u_2} {n : ℕ} (H : Π (t₁ : finset α), (Π {t₂ : finset α}, t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : finset α) :
s.card ≤ n → p s

Suppose that, given that p t can be defined on all supersets of s of cardinality less than n, one knows how to define p s. Then one can inductively define p s for all finsets s of cardinality less than n, starting from finsets of card n and iterating. This can be used either to define data, or to prove properties.

Equations
source
theorem finset.strong_downward_induction_eq {α : Type u_1} {n : ℕ} {p : finset α → Sort u_2} (H : Π (t₁ : finset α), (Π {t₂ : finset α}, t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : finset α) :
finset.strong_downward_induction H s = H s (λ (t : finset α) (ht : t.card ≤ n) (hst : s ⊂ t), finset.strong_downward_induction H t ht)
source
def finset.strong_downward_induction_on {α : Type u_1} {n : ℕ} {p : finset α → Sort u_2} (s : finset α) (H : Π (t₁ : finset α), (Π {t₂ : finset α}, t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) :
s.card ≤ n → p s

Analogue of strong_downward_induction with order of arguments swapped.

Equations
source
theorem finset.strong_downward_induction_on_eq {α : Type u_1} {n : ℕ} {p : finset α → Sort u_2} (s : finset α) (H : Π (t₁ : finset α), (Π {t₂ : finset α}, t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) :
s.strong_downward_induction_on H = H s (λ (t : finset α) (ht : t.card ≤ n) (h : s ⊂ t), t.strong_downward_induction_on H ht)
source
theorem finset.lt_wf {α : Type u_1} :
well_founded has_lt.lt