# Cardinality of a finite set #

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

## Main declarations #

- `Finset.card`: `#s : ℕ` returns the cardinality of `s : Finset α`.

### Induction principles #

- `Finset.strongInduction`: Strong induction
- `Finset.strongInductionOn`
- `Finset.strongDownwardInduction`
- `Finset.strongDownwardInductionOn`
- `Finset.case_strong_induction_on`
- `Finset.Nonempty.strong_induction`
- `Finset.eraseInduction`

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

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

The notation `#s` can be accessed in the `Finset` locale.

Equations

- s.card = s.val.card

Instances For

source
def Finset.«term#_» :
Lean.ParserDescr

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

The notation `#s` can be accessed in the `Finset` locale.

Equations

- Finset.«term#_» = Lean.ParserDescr.node `Finset.«term#_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1023))

Instances For

source
theorem Finset.card_def {α : Type u_1} (s : Finset α) :
s.card = s.val.card
source
@[simp]
theorem Finset.card_val {α : Type u_1} (s : Finset α) :
s.val.card = s.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
theorem Finset.card_le_card {α : Type u_1} {s t : Finset α} :
s ⊆ t → s.card ≤ t.card
source
theorem Finset.card_mono {α : Type u_1} :
Monotone card
source
@[simp]
theorem Finset.card_eq_zero {α : Type u_1} {s : Finset α} :
s.card = 0 ↔ s = ∅
source
theorem Finset.card_ne_zero {α : Type u_1} {s : Finset α} :
s.card ≠ 0 ↔ s.Nonempty
source
@[simp]
theorem Finset.card_pos {α : Type u_1} {s : Finset α} :
0 < s.card ↔ s.Nonempty
source
@[simp]
theorem Finset.one_le_card {α : Type u_1} {s : Finset α} :
1 ≤ 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.Nonempty.card_ne_zero {α : Type u_1} {s : Finset α} :
s.Nonempty → s.card ≠ 0

Alias of the reverse direction of `Finset.card_ne_zero`.

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 : α} [DecidableEq α] :
({a} ∩ s).card ≤ 1
source
@[simp]
theorem Finset.card_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) :
(cons a s h).card = s.card + 1
source
@[simp]
theorem Finset.card_insert_of_notMem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (h : a ∉ s) :
(insert a s).card = s.card + 1
source
@[deprecated Finset.card_insert_of_notMem (since := "2025-05-23")]
theorem Finset.card_insert_of_not_mem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (h : a ∉ s) :
(insert a s).card = s.card + 1

Alias of `Finset.card_insert_of_notMem`.

source
theorem Finset.card_insert_of_mem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (h : a ∈ s) :
(insert a s).card = s.card
source
theorem Finset.card_insert_le {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
(insert a s).card ≤ s.card + 1
source
theorem Finset.card_le_two {α : Type u_1} [DecidableEq α] {a b : α} :
{a, b}.card ≤ 2
source
theorem Finset.card_le_three {α : Type u_1} [DecidableEq α] {a b c : α} :
{a, b, c}.card ≤ 3
source
theorem Finset.card_le_four {α : Type u_1} [DecidableEq α] {a b c d : α} :
{a, b, c, d}.card ≤ 4
source
theorem Finset.card_le_five {α : Type u_1} [DecidableEq α] {a b c d e : α} :
{a, b, c, d, e}.card ≤ 5
source
theorem Finset.card_le_six {α : Type u_1} [DecidableEq α] {a b c d e f : α} :
{a, b, c, d, e, f}.card ≤ 6
source
theorem Finset.card_insert_eq_ite {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
(insert a s).card = if a ∈ s then s.card else s.card + 1

If `a ∈ s` is known, see also `Finset.card_insert_of_mem` and `Finset.card_insert_of_notMem`.

source
@[simp]
theorem Finset.card_pair_eq_one_or_two {α : Type u_1} {a b : α} [DecidableEq α] :
{a, b}.card = 1 ∨ {a, b}.card = 2
source
theorem Finset.card_pair {α : Type u_1} {a b : α} [DecidableEq α] (h : a ≠ b) :
{a, b}.card = 2
source
@[simp]
theorem Finset.card_erase_of_mem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
a ∈ s → (s.erase a).card = s.card - 1

$\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$.

source
theorem Finset.card_erase_add_one {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
a ∈ s → (s.erase a).card + 1 = s.card
source
theorem Finset.card_erase_lt_of_mem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
a ∈ s → (s.erase a).card < s.card
source
theorem Finset.card_erase_le {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
(s.erase a).card ≤ s.card
source
theorem Finset.pred_card_le_card_erase {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
s.card - 1 ≤ (s.erase a).card
source
theorem Finset.card_erase_eq_ite {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
(s.erase a).card = if a ∈ s then s.card - 1 else s.card

If `a ∈ s` is known, see also `Finset.card_erase_of_mem` and `Finset.erase_eq_of_notMem`.

source
@[simp]
theorem Finset.card_range (n : ℕ) :
(range n).card = n
source
@[simp]
theorem Finset.card_attach {α : Type u_1} {s : Finset α} :
s.attach.card = s.card
source
theorem Multiset.card_toFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) :
m.toFinset.card = m.dedup.card
source
theorem Multiset.toFinset_card_le {α : Type u_1} [DecidableEq α] (m : Multiset α) :
m.toFinset.card ≤ m.card
source
theorem Multiset.toFinset_card_of_nodup {α : Type u_1} [DecidableEq α] {m : Multiset α} (h : m.Nodup) :
m.toFinset.card = m.card
source
theorem Multiset.dedup_card_eq_card_iff_nodup {α : Type u_1} [DecidableEq α] {m : Multiset α} :
m.dedup.card = m.card ↔ m.Nodup
source
theorem Multiset.toFinset_card_eq_card_iff_nodup {α : Type u_1} [DecidableEq α] {m : Multiset α} :
m.toFinset.card = m.card ↔ m.Nodup
source
theorem List.card_toFinset {α : Type u_1} [DecidableEq α] (l : List α) :
l.toFinset.card = l.dedup.length
source
theorem List.toFinset_card_le {α : Type u_1} [DecidableEq α] (l : List α) :
l.toFinset.card ≤ l.length
source
theorem List.toFinset_card_of_nodup {α : Type u_1} [DecidableEq α] {l : List α} (h : l.Nodup) :
l.toFinset.card = l.length
source
@[simp]
theorem Finset.length_toList {α : Type u_1} (s : Finset α) :
s.toList.length = s.card
source
theorem Finset.card_image_le {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] :
(image f s).card ≤ s.card
source
theorem Finset.card_image_of_injOn {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] (H : Set.InjOn f ↑s) :
(image f s).card = s.card
source
theorem Finset.injOn_of_card_image_eq {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] (H : (image f s).card = s.card) :
Set.InjOn f ↑s
source
theorem Finset.card_image_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] :
(image f s).card = s.card ↔ Set.InjOn f ↑s
source
theorem Finset.card_image_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} [DecidableEq β] (s : Finset α) (H : Function.Injective f) :
(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 : α → β) [DecidableEq β] (y : β) :
{x ∈ s | f x = y}.card ≠ 0 ↔ y ∈ image f s
source
theorem Finset.card_filter_le_iff {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
(filter P s).card ≤ n ↔ ∀ s' ⊆ s, n < s'.card → ∃ a ∈ s', ¬P a
source
@[simp]
theorem Finset.card_map {α : Type u_1} {β : Type u_2} {s : Finset α} (f : α ↪ β) :
(map f s).card = s.card
source
@[simp]
theorem Finset.card_subtype {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) :
(Finset.subtype p s).card = (filter p s).card
source
theorem Finset.card_filter_le {α : Type u_1} (s : Finset α) (p : α → Prop) [DecidablePred p] :
(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_iff_card_le_of_subset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) :
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.eq_iff_card_ge_of_superset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) :
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 : map f s ⊆ s) :
map f s = s
source
theorem Finset.card_filter_eq_iff {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] :
(filter p s).card = s.card ↔ ∀ x ∈ s, p x
source
theorem Finset.filter_card_eq {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] :
(filter p s).card = s.card → ∀ x ∈ s, p x

Alias of the forward direction of `Finset.card_filter_eq_iff`.

source
theorem Finset.card_filter_eq_zero_iff {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] :
(filter p s).card = 0 ↔ ∀ 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_strictMono {α : Type u_1} :
StrictMono card
source
theorem Finset.card_eq_of_bijective {α : Type u_1} {s : Finset α} {n : ℕ} (f : (i : ℕ) → i < n → α) (hf : ∀ 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

See also `card_bij`. TODO: consider deprecating, since this has been unused in mathlib for a long time and is just a special case of `card_bij`.

source
theorem Finset.card_bij {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : (a : α) → a ∈ s → β) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b) :
s.card = t.card

Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t` are equal.

The difference with `Finset.card_bij'` is that the bijection is specified as a surjective injection, rather than by an inverse function.

The difference with `Finset.card_nbij` is that the bijection is allowed to use membership of the domain, rather than being a non-dependent function.

source
theorem Finset.card_bij' {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : (a : α) → a ∈ s → β) (j : (a : β) → a ∈ t → α) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s) (left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a) (right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a) :
s.card = t.card

Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t` are equal.

The difference with `Finset.card_bij` is that the bijection is specified with an inverse, rather than as a surjective injection.

The difference with `Finset.card_nbij'` is that the bijection and its inverse are allowed to use membership of the domains, rather than being non-dependent functions.

source
theorem Finset.card_nbij {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : α → β) (hi : Set.MapsTo i ↑s ↑t) (i_inj : Set.InjOn i ↑s) (i_surj : Set.SurjOn i ↑s ↑t) :
s.card = t.card

Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t` are equal.

The difference with `Finset.card_nbij'` is that the bijection is specified as a surjective injection, rather than by an inverse function.

The difference with `Finset.card_bij` is that the bijection is a non-dependent function, rather than being allowed to use membership of the domain.

source
theorem Finset.card_nbij' {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : α → β) (j : β → α) (hi : Set.MapsTo i ↑s ↑t) (hj : Set.MapsTo j ↑t ↑s) (left_inv : Set.LeftInvOn j i ↑s) (right_inv : Set.RightInvOn j i ↑t) :
s.card = t.card

Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t` are equal.

The difference with `Finset.card_nbij` is that the bijection is specified with an inverse, rather than as a surjective injection.

The difference with `Finset.card_bij'` is that the bijection and its inverse are non-dependent functions, rather than being allowed to use membership of the domains.

The difference with `Finset.card_equiv` is that bijectivity is only required to hold on the domains, rather than on the entire types.

source
theorem Finset.card_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (e : α ≃ β) (hst : ∀ (i : α), i ∈ s ↔ e i ∈ t) :
s.card = t.card

Specialization of `Finset.card_nbij'` that automatically fills in most arguments.

See `Fintype.card_equiv` for the version where `s` and `t` are `univ`.

source
theorem Finset.card_bijective {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (e : α → β) (he : Function.Bijective e) (hst : ∀ (i : α), i ∈ s ↔ e i ∈ t) :
s.card = t.card

Specialization of `Finset.card_nbij` that automatically fills in most arguments.

See `Fintype.card_bijective` for the version where `s` and `t` are `univ`.

source
theorem Set.BijOn.finsetCard_eq {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (e : α → β) (he : BijOn e ↑s ↑t) :
s.card = t.card
source
theorem Finset.card_le_card_of_injOn {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.MapsTo f ↑s ↑t) (f_inj : Set.InjOn f ↑s) :
s.card ≤ t.card
source
theorem Finset.card_le_card_of_injective {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : ↥s → ↥t} (hf : Function.Injective f) :
s.card ≤ t.card
source
theorem Finset.card_le_card_of_surjOn {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.SurjOn f ↑s ↑t) :
t.card ≤ s.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 : Set.MapsTo f ↑s ↑t) :
∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

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

See also `Set.exists_ne_map_eq_of_encard_lt_of_maps_to` and `Set.exists_ne_map_eq_of_ncard_lt_of_maps_to`.

source
theorem Finset.exists_ne_map_eq_of_card_image_lt {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] {f : α → β} (hc : (image f s).card < s.card) :
∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

a special case of `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` where `t` is `s.image f`

source
theorem Finset.not_injOn_of_card_image_lt {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] {f : α → β} (hc : (image f s).card < s.card) :
¬Set.InjOn f ↑s

a variant of `Finset.exists_ne_map_eq_of_card_image_lt` using `Set.InjOn`

source
theorem Finset.le_card_of_inj_on_range {α : Type u_1} {s : Finset α} {n : ℕ} (f : ℕ → α) (hf : ∀ i < n, f i ∈ s) (f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j) :
n ≤ s.card

See also `Finset.card_le_card_of_injOn`, which is a more general version of this lemma. TODO: consider deprecating, since this is just a special case of `Finset.card_le_card_of_injOn`.

source
theorem Finset.surjOn_of_injOn_of_card_le {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.MapsTo f ↑s ↑t) (hinj : Set.InjOn f ↑s) (hst : t.card ≤ s.card) :
Set.SurjOn f ↑s ↑t

Given an injective map `f` from a finite set `s` to another finite set `t`, if `t` is no larger than `s`, then `f` is surjective to `t` when restricted to `s`. See `Finset.surj_on_of_inj_on_of_card_le` for the version where `f` is a dependent function.

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

Given an injective map `f` defined on a finite set `s` to another finite set `t`, if `t` is no larger than `s`, then `f` is surjective to `t` when restricted to `s`. See `Finset.surjOn_of_injOn_of_card_le` for the version where `f` is a non-dependent function.

source
theorem Finset.injOn_of_surjOn_of_card_le {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.MapsTo f ↑s ↑t) (hsurj : Set.SurjOn f ↑s ↑t) (hst : s.card ≤ t.card) :
Set.InjOn f ↑s

Given a surjective map `f` from a finite set `s` to another finite set `t`, if `s` is no larger than `t`, then `f` is injective when restricted to `s`. See `Finset.inj_on_of_surj_on_of_card_le` for the version where `f` is a dependent function.

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 ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b) (hst : s.card ≤ t.card) ⦃a₁ : α⦄ (ha₁ : a₁ ∈ s) ⦃a₂ : α⦄ (ha₂ : a₂ ∈ s) (ha₁a₂ : f a₁ ha₁ = f a₂ ha₂) :
a₁ = a₂

Given a surjective map `f` defined on a finite set `s` to another finite set `t`, if `s` is no larger than `t`, then `f` is injective when restricted to `s`. See `Finset.injOn_of_surjOn_of_card_le` for the version where `f` is a non-dependent function.

source
@[simp]
theorem Finset.card_disjUnion {α : Type u_1} (s t : Finset α) (h : Disjoint s t) :
(s.disjUnion t h).card = s.card + t.card

### Lattice structure #

source
theorem Finset.card_union_add_card_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t).card + (s ∩ t).card = s.card + t.card
source
theorem Finset.card_inter_add_card_union {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∩ t).card + (s ∪ t).card = s.card + t.card
source
theorem Finset.card_union {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t).card = s.card + t.card - (s ∩ t).card
source
theorem Finset.card_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∩ t).card = s.card + t.card - (s ∪ t).card
source
theorem Finset.card_union_le {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t).card ≤ s.card + t.card
source
theorem Finset.card_union_eq_card_add_card {α : Type u_1} {s t : Finset α} [DecidableEq α] :
(s ∪ t).card = s.card + t.card ↔ Disjoint s t
source
@[simp]
theorem Finset.card_union_of_disjoint {α : Type u_1} {s t : Finset α} [DecidableEq α] :
Disjoint s t → (s ∪ t).card = s.card + t.card

Alias of the reverse direction of `Finset.card_union_eq_card_add_card`.

source
theorem Finset.card_sdiff_of_subset {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⊆ t) :
(t \ s).card = t.card - s.card
source
theorem Finset.card_sdiff {α : Type u_1} {s t : Finset α} [DecidableEq α] :
(t \ s).card = t.card - (s ∩ t).card
source
theorem Finset.card_sdiff_add_card_eq_card {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) :
(t \ s).card + s.card = t.card
source
theorem Finset.le_card_sdiff {α : Type u_1} [DecidableEq α] (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 α} [DecidableEq α] :
s.card ≤ (s \ t).card + t.card
source
theorem Finset.card_sdiff_add_card {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s \ t).card + t.card = (s ∪ t).card
source
theorem Finset.sdiff_nonempty_of_card_lt_card {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s.card < t.card) :
(t \ s).Nonempty
source
theorem Finset.exists_mem_notMem_of_card_lt_card {α : Type u_1} {s t : Finset α} (h : s.card < t.card) :
∃ e ∈ t, e ∉ s
source
@[deprecated Finset.exists_mem_notMem_of_card_lt_card (since := "2025-05-23")]
theorem Finset.exists_mem_not_mem_of_card_lt_card {α : Type u_1} {s t : Finset α} (h : s.card < t.card) :
∃ e ∈ t, e ∉ s

Alias of `Finset.exists_mem_notMem_of_card_lt_card`.

source
@[simp]
theorem Finset.card_sdiff_add_card_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s \ t).card + (s ∩ t).card = s.card
source
@[simp]
theorem Finset.card_inter_add_card_sdiff {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∩ t).card + (s \ t).card = s.card
source
theorem Finset.card_sdiff_le_card_sdiff_iff {α : Type u_1} {s t : Finset α} [DecidableEq α] :
(s \ t).card ≤ (t \ s).card ↔ s.card ≤ t.card
source
theorem Finset.card_sdiff_lt_card_sdiff_iff {α : Type u_1} {s t : Finset α} [DecidableEq α] :
(s \ t).card < (t \ s).card ↔ s.card < t.card
source
theorem Finset.card_sdiff_eq_card_sdiff_iff {α : Type u_1} {s t : Finset α} [DecidableEq α] :
(s \ t).card = (t \ s).card ↔ s.card = t.card
source
theorem Finset.card_sdiff_comm {α : Type u_1} {s t : Finset α} [DecidableEq α] :
s.card = t.card → (s \ t).card = (t \ s).card

Alias of the reverse direction of `Finset.card_sdiff_eq_card_sdiff_iff`.

source
theorem Finset.inter_nonempty_of_card_lt_card_add_card {α : Type u_1} {s t u : Finset α} [DecidableEq α] (hts : t ⊆ s) (hus : u ⊆ s) (hstu : s.card < t.card + u.card) :
(t ∩ u).Nonempty

Pigeonhole principle for two finsets inside an ambient finset.

source
theorem Finset.filter_card_add_filter_neg_card_eq_card {α : Type u_1} {s : Finset α} (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] :
(filter p s).card + {a ∈ s | ¬p a}.card = s.card
source
theorem Finset.exists_subsuperset_card_eq {α : Type u_1} {s t : Finset α} {n : ℕ} (hst : s ⊆ t) (hsn : s.card ≤ n) (hnt : n ≤ t.card) :
∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ u.card = n

Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a set `u` of size `n` which is both a superset of `s` and a subset of `t`.

source
theorem Finset.exists_subset_card_eq {α : Type u_1} {s : Finset α} {n : ℕ} (hns : n ≤ s.card) :
∃ t ⊆ s, t.card = n

We can shrink a set to any smaller size.

source
theorem Finset.le_card_iff_exists_subset_card {α : Type u_1} {s : Finset α} {n : ℕ} :
n ≤ s.card ↔ ∃ t ⊆ s, t.card = n
source
theorem Finset.exists_subset_or_subset_of_two_mul_lt_card {α : Type u_1} [DecidableEq α] {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} [DecidableEq α] {s t : Finset α} :
(∃ a ∉ s, 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 ∈ s, ∀ 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_subsingleton_coe {α : Type u_1} {s : Finset α} :
s.card ≤ 1 ↔ Subsingleton ↥s
source
theorem Finset.card_le_one_iff_subset_singleton {α : Type u_1} {s : Finset α} [Nonempty α] :
s.card ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
source
theorem Finset.exists_mem_ne {α : Type u_1} {s : Finset α} (hs : 1 < s.card) (a : α) :
∃ b ∈ s, b ≠ a
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 ∈ s, ∃ 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.one_lt_card_iff_nontrivial {α : Type u_1} {s : Finset α} :
1 < s.card ↔ s.Nontrivial
source
@[deprecated Finset.exists_mem_ne (since := "2025-08-14")]
theorem Finset.exists_ne_of_one_lt_card {α : Type u_1} {s : Finset α} (hs : 1 < s.card) (a : α) :
∃ b ∈ s, b ≠ a

Alias of `Finset.exists_mem_ne`.

source
theorem Finset.exists_of_one_lt_card_pi {ι : Type u_4} {α : ι → Type u_5} [(i : ι) → DecidableEq (α i)] {s : Finset ((i : ι) → α i)} (h : 1 < s.card) :
∃ (i : ι), 1 < (image (fun (x : (i : ι) → α i) => x i) s).card ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

If a Finset in a Pi type is nontrivial (has at least two elements), then its projection to some factor is nontrivial, and the fibers of the projection are proper subsets.

source
theorem Finset.card_eq_succ_iff_cons {α : Type u_1} {s : Finset α} {n : ℕ} :
s.card = n + 1 ↔ ∃ (a : α) (t : Finset α) (h : a ∉ t), cons a t h = s ∧ t.card = n
source
theorem Finset.card_eq_succ {α : Type u_1} {s : Finset α} {n : ℕ} [DecidableEq α] :
s.card = n + 1 ↔ ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ t.card = n
source
theorem Finset.card_eq_two {α : Type u_1} {s : Finset α} [DecidableEq α] :
s.card = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
source
theorem Finset.card_eq_three {α : Type u_1} {s : Finset α} [DecidableEq α] :
s.card = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
source
theorem Finset.card_eq_four {α : Type u_1} {s : Finset α} [DecidableEq α] :
s.card = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
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 ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
source
theorem Finset.three_lt_card_iff {α : Type u_1} {s : Finset α} :
3 < s.card ↔ ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
source
theorem Finset.three_lt_card {α : Type u_1} {s : Finset α} :
3 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

### Inductions #

source
@[irreducible]
def Finset.strongInduction {α : Type u_1} {p : Finset α → Sort u_4} (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

- Finset.strongInduction H x✝ = H x✝ fun (t : Finset α) (h : t ⊂ x✝) => have this := ⋯; Finset.strongInduction H t

Instances For

source
theorem Finset.strongInduction_eq {α : Type u_1} {p : Finset α → Sort u_4} (H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) (s : Finset α) :
strongInduction H s = H s fun (t : Finset α) (x : t ⊂ s) => strongInduction H t
source
def Finset.strongInductionOn {α : Type u_1} {p : Finset α → Sort u_4} (s : Finset α) :
((s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) → p s

Analogue of `strongInduction` with order of arguments swapped.

Equations

- s.strongInductionOn H = Finset.strongInduction H s

Instances For

source
theorem Finset.strongInductionOn_eq {α : Type u_1} {p : Finset α → Sort u_4} (s : Finset α) (H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) :
s.strongInductionOn H = H s fun (t : Finset α) (x : t ⊂ s) => t.strongInductionOn H
source
theorem Finset.case_strong_induction_on {α : Type u_1} [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h₀ : p ∅) (h₁ : ∀ (a : α) (s : Finset α), a ∉ s → (∀ t ⊆ s, p t) → p (insert a s)) :
p s
source
@[irreducible]
theorem Finset.Nonempty.strong_induction {α : Type u_1} {p : (s : Finset α) → s.Nonempty → Prop} (h₀ : ∀ (a : α), p {a} ⋯) (h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯) ⦃s : Finset α⦄ (hs : s.Nonempty) :
p s hs

Suppose that, given objects defined on all nonempty strict subsets of any nontrivial finset `s`, one knows how to define an object on `s`. Then one can inductively define an object on all finsets, starting from singletons and iterating.

TODO: Currently this can only be used to prove properties. Replace `Finset.Nonempty.exists_eq_singleton_or_nontrivial` with computational content in order to let `p` be `Sort`-valued.

source
@[irreducible]
def Finset.strongDownwardInduction {α : Type u_1} {p : Finset α → Sort u_4} {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

- Finset.strongDownwardInduction H x✝ = H x✝ fun {t : Finset α} (ht : t.card ≤ n) (h : x✝ ⊂ t) => have this := ⋯; have this := ⋯; Finset.strongDownwardInduction H t ht

Instances For

source
theorem Finset.strongDownwardInduction_eq {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4} (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Finset α) :
strongDownwardInduction H s = H s fun {t : Finset α} (ht : t.card ≤ n) (x : s ⊂ t) => strongDownwardInduction H t ht
source
def Finset.strongDownwardInductionOn {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4} (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 `strongDownwardInduction` with order of arguments swapped.

Equations

- s.strongDownwardInductionOn H = Finset.strongDownwardInduction H s

Instances For

source
theorem Finset.strongDownwardInductionOn_eq {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4} (s : Finset α) (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) :
(fun (a : s.card ≤ n) => s.strongDownwardInductionOn H a) = H s fun {t : Finset α} (ht : t.card ≤ n) (x : s ⊂ t) => t.strongDownwardInductionOn H ht
source
theorem Finset.lt_wf {α : Type u_4} :
WellFounded LT.lt
source
theorem Finset.eraseInduction {α : Type u_1} [DecidableEq α] {p : Finset α → Prop} (H : ∀ (S : Finset α), (∀ s ∈ S, p (S.erase s)) → p S) (S : Finset α) :
p S

To prove a proposition for an arbitrary `Finset α`, it suffices to prove that for any `S : Finset α`, the following is true: the property is true for S with any element `s` removed, then the property holds for `S`.

This is a weaker version of `Finset.strongInduction`. But it can be more precise when the induction argument only requires removing single elements at a time.