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

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.

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.

theorem Finset.card_def {α : Type u_1} (s : Finset α) : s.card = s.val.card

@[simp]

theorem Finset.card_val {α : Type u_1} (s : Finset α) : s.val.card = s.card

@[simp]

theorem Finset.card_mk {α : Type u_1} {m : Multiset α} {nodup : m.Nodup} : { val := m, nodup := nodup }.card = m.card

@[simp]

theorem Finset.card_empty {α : Type u_1} : ∅.card = 0

theorem Finset.card_le_card {α : Type u_1} {s t : Finset α} : s ⊆ t → s.card ≤ t.card

theorem Finset.card_mono {α : Type u_1} : Monotone card

@[simp]

theorem Finset.card_eq_zero {α : Type u_1} {s : Finset α} : s.card = 0 ↔ s = ∅

theorem Finset.card_ne_zero {α : Type u_1} {s : Finset α} : s.card ≠ 0 ↔ s.Nonempty

@[simp]

theorem Finset.card_pos {α : Type u_1} {s : Finset α} : 0 < s.card ↔ s.Nonempty

@[simp]

theorem Finset.one_le_card {α : Type u_1} {s : Finset α} : 1 ≤ s.card ↔ s.Nonempty

theorem Finset.Nonempty.card_pos {α : Type u_1} {s : Finset α} : s.Nonempty → 0 < s.card

Alias of the reverse direction of Finset.card_pos.

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.

theorem Finset.card_ne_zero_of_mem {α : Type u_1} {s : Finset α} {a : α} (h : a ∈ s) : s.card ≠ 0

@[simp]

theorem Finset.card_singleton {α : Type u_1} (a : α) : {a}.card = 1

theorem Finset.card_singleton_inter {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] : ({a} ∩ s).card ≤ 1

@[simp]

theorem Finset.card_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : (cons a s h).card = s.card + 1

@[simp]

theorem Finset.card_insert_of_notMem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (h : a ∉ s) : (insert a s).card = s.card + 1

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

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

theorem Finset.card_insert_le {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).card ≤ s.card + 1

theorem Finset.card_le_two {α : Type u_1} [DecidableEq α] {a b : α} : {a, b}.card ≤ 2

theorem Finset.card_le_three {α : Type u_1} [DecidableEq α] {a b c : α} : {a, b, c}.card ≤ 3

theorem Finset.card_le_four {α : Type u_1} [DecidableEq α] {a b c d : α} : {a, b, c, d}.card ≤ 4

theorem Finset.card_le_five {α : Type u_1} [DecidableEq α] {a b c d e : α} : {a, b, c, d, e}.card ≤ 5

theorem Finset.card_le_six {α : Type u_1} [DecidableEq α] {a b c d e f : α} : {a, b, c, d, e, f}.card ≤ 6

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.

@[simp]

theorem Finset.card_pair_eq_one_or_two {α : Type u_1} {a b : α} [DecidableEq α] : {a, b}.card = 1 ∨ {a, b}.card = 2

theorem Finset.card_pair {α : Type u_1} {a b : α} [DecidableEq α] (h : a ≠ b) : {a, b}.card = 2

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

theorem Finset.card_erase_add_one {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] : a ∈ s → (s.erase a).card + 1 = s.card

theorem Finset.card_erase_lt_of_mem {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] : a ∈ s → (s.erase a).card < s.card

theorem Finset.card_erase_le {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] : (s.erase a).card ≤ s.card

theorem Finset.pred_card_le_card_erase {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] : s.card - 1 ≤ (s.erase a).card

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.

@[simp]

theorem Finset.card_range (n : ℕ) : (range n).card = n

@[simp]

theorem Finset.card_attach {α : Type u_1} {s : Finset α} : s.attach.card = s.card

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

theorem Multiset.toFinset_card_le {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.toFinset.card ≤ m.card

theorem Multiset.toFinset_card_of_nodup {α : Type u_1} [DecidableEq α] {m : Multiset α} (h : m.Nodup) : m.toFinset.card = m.card

theorem Multiset.dedup_card_eq_card_iff_nodup {α : Type u_1} [DecidableEq α] {m : Multiset α} : m.dedup.card = m.card ↔ m.Nodup

theorem Multiset.toFinset_card_eq_card_iff_nodup {α : Type u_1} [DecidableEq α] {m : Multiset α} : m.toFinset.card = m.card ↔ m.Nodup

theorem List.card_toFinset {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset.card = l.dedup.length

theorem List.toFinset_card_le {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset.card ≤ l.length

theorem List.toFinset_card_of_nodup {α : Type u_1} [DecidableEq α] {l : List α} (h : l.Nodup) : l.toFinset.card = l.length

@[simp]

theorem Finset.length_toList {α : Type u_1} (s : Finset α) : s.toList.length = s.card

theorem Finset.card_image_le {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] : (image f s).card ≤ s.card

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

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

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

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

theorem Finset.fiber_card_ne_zero_iff_mem_image {α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → β) [DecidableEq β] (y : β) : (filter (fun (x : α) => f x = y) s).card ≠ 0 ↔ y ∈ image f s

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

@[simp]

theorem Finset.card_map {α : Type u_1} {β : Type u_2} {s : Finset α} (f : α ↪ β) : (map f s).card = s.card

@[simp]

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

theorem Finset.card_filter_le {α : Type u_1} (s : Finset α) (p : α → Prop) [DecidablePred p] : (filter p s).card ≤ s.card

theorem Finset.eq_of_subset_of_card_le {α : Type u_1} {s t : Finset α} (h : s ⊆ t) (h₂ : t.card ≤ s.card) : s = t

theorem Finset.eq_iff_card_le_of_subset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) : t.card ≤ s.card ↔ s = t

theorem Finset.eq_of_superset_of_card_ge {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) (hts : t.card ≤ s.card) : t = s

theorem Finset.eq_iff_card_ge_of_superset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) : t.card ≤ s.card ↔ t = s

theorem Finset.subset_iff_eq_of_card_le {α : Type u_1} {s t : Finset α} (h : t.card ≤ s.card) : s ⊆ t ↔ s = t

theorem Finset.map_eq_of_subset {α : Type u_1} {s : Finset α} {f : α ↪ α} (hs : map f s ⊆ s) : map f s = s

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

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.

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

theorem Finset.card_lt_card {α : Type u_1} {s t : Finset α} (h : s ⊂ t) : s.card < t.card

theorem Finset.card_strictMono {α : Type u_1} : StrictMono card

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.

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.

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.

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.

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.

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.

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.

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

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

theorem Finset.card_le_card_of_injective {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : { x : α // x ∈ s } → { x : β // x ∈ t }} (hf : Function.Injective f) : s.card ≤ t.card

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

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.

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.

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.

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.

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.

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.

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

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

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

theorem Finset.card_union {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t).card = s.card + t.card - (s ∩ t).card

theorem Finset.card_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∩ t).card = s.card + t.card - (s ∪ t).card

theorem Finset.card_union_le {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t).card ≤ s.card + t.card

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

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

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

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

theorem Finset.le_card_sdiff {α : Type u_1} [DecidableEq α] (s t : Finset α) : t.card - s.card ≤ (t \ s).card

theorem Finset.card_le_card_sdiff_add_card {α : Type u_1} {s t : Finset α} [DecidableEq α] : s.card ≤ (s \ t).card + t.card

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

theorem Finset.sdiff_nonempty_of_card_lt_card {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s.card < t.card) : (t \ s).Nonempty

theorem Finset.exists_mem_notMem_of_card_lt_card {α : Type u_1} {s t : Finset α} (h : s.card < t.card) : ∃ e ∈ t, e ∉ s

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

@[simp]

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

@[simp]

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

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

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

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

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.

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.

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 + (filter (fun (a : α) => ¬p a) s).card = s.card

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.

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.

theorem Finset.le_card_iff_exists_subset_card {α : Type u_1} {s : Finset α} {n : ℕ} : n ≤ s.card ↔ ∃ t ⊆ s, t.card = n

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

theorem Finset.card_eq_one {α : Type u_1} {s : Finset α} : s.card = 1 ↔ ∃ (a : α), s = {a}

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

theorem Finset.card_le_one {α : Type u_1} {s : Finset α} : s.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

theorem Finset.card_le_one_iff {α : Type u_1} {s : Finset α} : s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

theorem Finset.card_le_one_iff_subsingleton_coe {α : Type u_1} {s : Finset α} : s.card ≤ 1 ↔ Subsingleton { x : α // x ∈ s }

theorem Finset.card_le_one_iff_subset_singleton {α : Type u_1} {s : Finset α} [Nonempty α] : s.card ≤ 1 ↔ ∃ (x : α), s ⊆ {x}

theorem Finset.exists_mem_ne {α : Type u_1} {s : Finset α} (hs : 1 < s.card) (a : α) : ∃ b ∈ s, b ≠ a

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.

theorem Finset.one_lt_card {α : Type u_1} {s : Finset α} : 1 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

theorem Finset.one_lt_card_iff {α : Type u_1} {s : Finset α} : 1 < s.card ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

theorem Finset.one_lt_card_iff_nontrivial {α : Type u_1} {s : Finset α} : 1 < s.card ↔ s.Nontrivial

theorem Finset.exists_ne_of_one_lt_card {α : Type u_1} {s : Finset α} (hs : 1 < s.card) (a : α) : ∃ b ∈ s, b ≠ a

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), filter (fun (x : (i : ι) → α i) => x i = ai) s ⊂ 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.

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

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

theorem Finset.card_eq_two {α : Type u_1} {s : Finset α} [DecidableEq α] : s.card = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

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}

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}

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

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

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

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

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

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

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.

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

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

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

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

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

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.

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

theorem Finset.lt_wf {α : Type u_4} : WellFounded LT.lt

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.