Cardinality of a finite set

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

Main declarations

• Finset.card: s.card : ℕ 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

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

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

Equations

• s.card = Multiset.card s.val

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

theorem Finset.card_pos {α : Type u_1} {s : Finset α} : 0 < 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.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) : (Finset.cons a s h).card = s.card + 1

@[simp]

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

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

@[simp]

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

@[deprecated Finset.card_pair]

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

Alias of Finset.card_pair.

@[simp]

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

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

@[simp]

theorem Finset.cast_card_erase_of_mem {α : Type u_1} {a : α} [DecidableEq α] {R : Type u_4} [AddGroupWithOne R] {s : Finset α} (hs : a ∈ s) : ↑(Finset.erase s a).card = ↑s.card - 1

$#(s \setminus {a}) = #s - 1$ if $a \in s$. This result is casted to any additive group with 1, so that we don't have to work with ℕ-subtraction.

@[simp]

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

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

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

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

theorem Finset.card_erase_eq_ite {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] : (Finset.erase s 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_not_mem.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

theorem Finset.card_image_le {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] : (Finset.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) : (Finset.image f s).card = s.card

theorem Finset.injOn_of_card_image_eq {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [DecidableEq β] (H : (Finset.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 β] : (Finset.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) : (Finset.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 : β) : (Finset.filter (fun (x : α) => f x = y) s).card ≠ 0 ↔ y ∈ Finset.image f s

theorem Finset.card_filter_le_iff {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] (n : ℕ) : (Finset.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 : α ↪ β) : (Finset.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 = (Finset.filter p s).card

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

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

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

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

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

theorem Finset.filter_card_eq {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] (h : (Finset.filter p s).card = s.card) (x : α) (hx : x ∈ s) : p x

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

theorem Finset.card_strictMono {α : Type u_1} : StrictMono Finset.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

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

theorem Finset.card_le_card_of_inj_on {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : ∀ a₁ ∈ s, ∀ a₂ ∈ s, f a₁ = f a₂ → a₁ = a₂) : s.card ≤ t.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 : ∀ a ∈ s, f a ∈ 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.

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

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

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₂

@[simp]

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

Lattice structure

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

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

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

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

@[simp]

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

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

theorem Finset.cast_card_sdiff {α : Type u_1} {R : Type u_3} {s : Finset α} {t : Finset α} [DecidableEq α] [AddGroupWithOne R] (h : s ⊆ t) : ↑(t \ s).card = ↑t.card - ↑s.card

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem Finset.filter_card_add_filter_neg_card_eq_card {α : Type u_1} {s : Finset α} (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : (Finset.filter p s).card + (Finset.filter (fun (a : α) => ¬p a) s).card = s.card

theorem Finset.exists_intermediate_set {α : Type u_1} {A : Finset α} {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.

theorem Finset.exists_smaller_set {α : Type u_1} (A : Finset α) (i : ℕ) (h₁ : i ≤ A.card) : ∃ B ⊆ A, B.card = i

We can shrink A to any smaller size.

theorem Finset.exists_subset_or_subset_of_two_mul_lt_card {α : Type u_1} [DecidableEq α] {X : Finset α} {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 : Finset α} {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 ↔ Finset.Nontrivial s

@[deprecated Finset.one_lt_card_iff_nontrivial]

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

Alias of Finset.one_lt_card_iff_nontrivial.

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.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 < (Finset.image (fun (x : (i : ι) → α i) => x i) s).card ∧ ∀ (ai : α i), Finset.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 {α : 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}

Inductions

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) => let_fun this := (_ : t.card < x.card); Finset.strongInduction H t

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 α) : Finset.strongInduction H s = H s fun (t : Finset α) (x : t ⊂ s) => Finset.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.

Equations

• Finset.strongInductionOn s H = Finset.strongInduction H s

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) : Finset.strongInductionOn s H = H s fun (t : Finset α) (x : t ⊂ s) => Finset.strongInductionOn t 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

theorem Finset.Nonempty.strong_induction {α : Type u_1} {p : (s : Finset α) → s.Nonempty → Prop} (h₀ : ∀ (a : α), p {a} (_ : {a}.Nonempty)) (h₁ : ∀ ⦃s : Finset α⦄ (hs : Finset.Nontrivial s), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s (_ : Set.Nonempty ↑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.

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) => let_fun this := (_ : n - t.card < n - x.card); Finset.strongDownwardInduction H t ht

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 α) : Finset.strongDownwardInduction H s = H s fun {t : Finset α} (ht : t.card ≤ n) (x : s ⊂ t) => Finset.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.

Equations

• Finset.strongDownwardInductionOn s H = Finset.strongDownwardInduction H s

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) => Finset.strongDownwardInductionOn s H a) = H s fun {t : Finset α} (ht : t.card ≤ n) (x : s ⊂ t) => Finset.strongDownwardInductionOn t H ht

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

Deprecated lemmas

Those lemmas have been deprecated on 2023-12-27.

@[deprecated Finset.card_le_card]

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

Alias of Finset.card_le_card.