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 ofs : Finset α.
Induction principles #
Finset.strongInduction: Strong inductionFinset.strongInductionOnFinset.strongDownwardInductionFinset.strongDownwardInductionOnFinset.case_strong_induction_on
TODO #
Should we add a noncomputable version?
s.card is the number of elements of s, aka its cardinality.
Equations
- Finset.card s = ↑Multiset.card s.val
@[simp]
theorem
Finset.card_mk
{α : Type u_1}
{m : Multiset α}
{nodup : Multiset.Nodup m}
:
Finset.card { val := m, nodup := nodup } = ↑Multiset.card m
theorem
Finset.card_le_of_subset
{α : Type u_1}
{s : Finset α}
{t : Finset α}
:
s ⊆ t → Finset.card s ≤ Finset.card t
@[simp]
theorem
Finset.Nonempty.card_pos
{α : Type u_1}
{s : Finset α}
:
Finset.Nonempty s → 0 < Finset.card s
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)
:
Finset.card s ≠ 0
theorem
Finset.card_singleton_inter
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
Finset.card ({a} ∩ s) ≤ 1
@[simp]
theorem
Finset.card_cons
{α : Type u_1}
{s : Finset α}
{a : α}
(h : ¬a ∈ s)
:
Finset.card (Finset.cons a s h) = Finset.card s + 1
@[simp]
theorem
Finset.card_insert_of_not_mem
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
(h : ¬a ∈ s)
:
Finset.card (insert a s) = Finset.card s + 1
theorem
Finset.card_insert_of_mem
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
(h : a ∈ s)
:
Finset.card (insert a s) = Finset.card s
theorem
Finset.card_insert_le
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(s : Finset α)
:
Finset.card (insert a s) ≤ Finset.card s + 1
theorem
Finset.card_insert_eq_ite
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
Finset.card (insert a s) = if a ∈ s then Finset.card s else Finset.card s + 1
If a ∈ s∈ s is known, see also Finset.card_insert_of_mem and Finset.card_insert_of_not_mem.
@[simp]
theorem
Finset.card_doubleton
{α : Type u_1}
{a : α}
{b : α}
[inst : DecidableEq α]
(h : a ≠ b)
:
Finset.card {a, b} = 2
@[simp]
theorem
Finset.card_erase_of_mem
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
a ∈ s → Finset.card (Finset.erase s a) = Finset.card s - 1
@[simp]
theorem
Finset.card_erase_add_one
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
a ∈ s → Finset.card (Finset.erase s a) + 1 = Finset.card s
theorem
Finset.card_erase_lt_of_mem
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
a ∈ s → Finset.card (Finset.erase s a) < Finset.card s
theorem
Finset.card_erase_le
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
Finset.card (Finset.erase s a) ≤ Finset.card s
theorem
Finset.pred_card_le_card_erase
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
Finset.card s - 1 ≤ Finset.card (Finset.erase s a)
theorem
Finset.card_erase_eq_ite
{α : Type u_1}
{s : Finset α}
{a : α}
[inst : DecidableEq α]
:
Finset.card (Finset.erase s a) = if a ∈ s then Finset.card s - 1 else Finset.card s
If a ∈ s∈ s is known, see also Finset.card_erase_of_mem and Finset.erase_eq_of_not_mem.
@[simp]
theorem
Finset.card_attach
{α : Type u_1}
{s : Finset α}
:
Finset.card (Finset.attach s) = Finset.card s
theorem
Multiset.card_toFinset
{α : Type u_1}
[inst : DecidableEq α]
(m : Multiset α)
:
Finset.card (Multiset.toFinset m) = ↑Multiset.card (Multiset.dedup m)
theorem
Multiset.toFinset_card_le
{α : Type u_1}
[inst : DecidableEq α]
(m : Multiset α)
:
Finset.card (Multiset.toFinset m) ≤ ↑Multiset.card m
theorem
Multiset.toFinset_card_of_nodup
{α : Type u_1}
[inst : DecidableEq α]
{m : Multiset α}
(h : Multiset.Nodup m)
:
Finset.card (Multiset.toFinset m) = ↑Multiset.card m
theorem
List.card_toFinset
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
:
Finset.card (List.toFinset l) = List.length (List.dedup l)
theorem
List.toFinset_card_le
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
:
Finset.card (List.toFinset l) ≤ List.length l
theorem
List.toFinset_card_of_nodup
{α : Type u_1}
[inst : DecidableEq α]
{l : List α}
(h : List.Nodup l)
:
Finset.card (List.toFinset l) = List.length l
@[simp]
theorem
Finset.length_toList
{α : Type u_1}
(s : Finset α)
:
List.length (Finset.toList s) = Finset.card s
theorem
Finset.card_image_le
{α : Type u_2}
{β : Type u_1}
{s : Finset α}
{f : α → β}
[inst : DecidableEq β]
:
Finset.card (Finset.image f s) ≤ Finset.card s
theorem
Finset.card_image_of_injOn
{α : Type u_2}
{β : Type u_1}
{s : Finset α}
{f : α → β}
[inst : DecidableEq β]
(H : Set.InjOn f ↑s)
:
Finset.card (Finset.image f s) = Finset.card s
theorem
Finset.injOn_of_card_image_eq
{α : Type u_2}
{β : Type u_1}
{s : Finset α}
{f : α → β}
[inst : DecidableEq β]
(H : Finset.card (Finset.image f s) = Finset.card s)
:
Set.InjOn f ↑s
theorem
Finset.card_image_iff
{α : Type u_2}
{β : Type u_1}
{s : Finset α}
{f : α → β}
[inst : DecidableEq β]
:
Finset.card (Finset.image f s) = Finset.card s ↔ Set.InjOn f ↑s
theorem
Finset.card_image_of_injective
{α : Type u_2}
{β : Type u_1}
{f : α → β}
[inst : DecidableEq β]
(s : Finset α)
(H : Function.Injective f)
:
Finset.card (Finset.image f s) = Finset.card s
theorem
Finset.fiber_card_ne_zero_iff_mem_image
{α : Type u_1}
{β : Type u_2}
(s : Finset α)
(f : α → β)
[inst : DecidableEq β]
(y : β)
:
Finset.card (Finset.filter (fun x => f x = y) s) ≠ 0 ↔ y ∈ Finset.image f s
@[simp]
theorem
Finset.card_map
{α : Type u_1}
{β : Type u_2}
{s : Finset α}
(f : α ↪ β)
:
Finset.card (Finset.map f s) = Finset.card s
@[simp]
theorem
Finset.card_subtype
{α : Type u_1}
(p : α → Prop)
[inst : DecidablePred p]
(s : Finset α)
:
Finset.card (Finset.subtype p s) = Finset.card (Finset.filter p s)
theorem
Finset.card_filter_le
{α : Type u_1}
(s : Finset α)
(p : α → Prop)
[inst : DecidablePred p]
:
Finset.card (Finset.filter p s) ≤ Finset.card s
theorem
Finset.eq_of_subset_of_card_le
{α : Type u_1}
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
(h₂ : Finset.card t ≤ Finset.card s)
:
s = t
theorem
Finset.eq_of_superset_of_card_ge
{α : Type u_1}
{s : Finset α}
{t : Finset α}
(hst : s ⊆ t)
(hts : Finset.card t ≤ Finset.card s)
:
t = s
theorem
Finset.subset_iff_eq_of_card_le
{α : Type u_1}
{s : Finset α}
{t : Finset α}
(h : Finset.card t ≤ Finset.card s)
:
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}
[inst : DecidablePred p]
(h : Finset.card (Finset.filter p s) = Finset.card s)
(x : α)
(hx : x ∈ s)
:
p x
theorem
Finset.card_lt_card
{α : Type u_1}
{s : Finset α}
{t : Finset α}
(h : s ⊂ t)
:
Finset.card s < Finset.card t
theorem
Finset.exists_ne_map_eq_of_card_lt_of_maps_to
{α : Type u_2}
{β : Type u_1}
{s : Finset α}
{t : Finset β}
(hc : Finset.card t < Finset.card s)
{f : α → β}
(hf : ∀ (a : α), a ∈ s → f a ∈ t)
:
If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.
theorem
Finset.surj_on_of_inj_on_of_card_le
{α : Type u_2}
{β : Type u_1}
{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 : Finset.card t ≤ Finset.card s)
(b : β)
:
theorem
Finset.inj_on_of_surj_on_of_card_le
{α : Type u_2}
{β : Type u_1}
{s : Finset α}
{t : Finset β}
(f : (a : α) → a ∈ s → β)
(hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t)
(hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha)
(hst : Finset.card s ≤ Finset.card t)
⦃a₁ : α⦄
⦃a₂ : α⦄
(ha₁ : a₁ ∈ s)
(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.card (Finset.disjUnion s t h) = Finset.card s + Finset.card t
Lattice structure #
theorem
Finset.card_union_add_card_inter
{α : Type u_1}
[inst : DecidableEq α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ∪ t) + Finset.card (s ∩ t) = Finset.card s + Finset.card t
theorem
Finset.card_inter_add_card_union
{α : Type u_1}
[inst : DecidableEq α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ∩ t) + Finset.card (s ∪ t) = Finset.card s + Finset.card t
theorem
Finset.card_union_le
{α : Type u_1}
[inst : DecidableEq α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ∪ t) ≤ Finset.card s + Finset.card t
theorem
Finset.card_union_eq
{α : Type u_1}
{s : Finset α}
{t : Finset α}
[inst : DecidableEq α]
(h : Disjoint s t)
:
Finset.card (s ∪ t) = Finset.card s + Finset.card t
@[simp]
theorem
Finset.card_disjoint_union
{α : Type u_1}
{s : Finset α}
{t : Finset α}
[inst : DecidableEq α]
(h : Disjoint s t)
:
Finset.card (s ∪ t) = Finset.card s + Finset.card t
theorem
Finset.card_sdiff
{α : Type u_1}
{s : Finset α}
{t : Finset α}
[inst : DecidableEq α]
(h : s ⊆ t)
:
Finset.card (t \ s) = Finset.card t - Finset.card s
theorem
Finset.card_sdiff_add_card_eq_card
{α : Type u_1}
[inst : DecidableEq α]
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
:
Finset.card (t \ s) + Finset.card s = Finset.card t
theorem
Finset.le_card_sdiff
{α : Type u_1}
[inst : DecidableEq α]
(s : Finset α)
(t : Finset α)
:
Finset.card t - Finset.card s ≤ Finset.card (t \ s)
theorem
Finset.card_le_card_sdiff_add_card
{α : Type u_1}
{s : Finset α}
{t : Finset α}
[inst : DecidableEq α]
:
Finset.card s ≤ Finset.card (s \ t) + Finset.card t
theorem
Finset.card_sdiff_add_card
{α : Type u_1}
{s : Finset α}
{t : Finset α}
[inst : DecidableEq α]
:
Finset.card (s \ t) + Finset.card t = Finset.card (s ∪ t)
theorem
Finset.filter_card_add_filter_neg_card_eq_card
{α : Type u_1}
{s : Finset α}
(p : α → Prop)
[inst : DecidablePred p]
[inst : (x : α) → Decidable ¬p x]
:
Finset.card (Finset.filter p s) + Finset.card (Finset.filter (fun a => ¬p a) s) = Finset.card s
theorem
Finset.exists_intermediate_set
{α : Type u_1}
{A : Finset α}
{B : Finset α}
(i : ℕ)
(h₁ : i + Finset.card B ≤ Finset.card A)
(h₂ : B ⊆ A)
:
∃ C, B ⊆ C ∧ C ⊆ A ∧ Finset.card C = i + Finset.card B
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 ≤ Finset.card A)
:
∃ B, B ⊆ A ∧ Finset.card B = i
We can shrink A to any smaller size.
theorem
Finset.exists_subset_or_subset_of_two_mul_lt_card
{α : Type u_1}
[inst : DecidableEq α]
{X : Finset α}
{Y : Finset α}
{n : ℕ}
(hXY : 2 * n < Finset.card (X ∪ Y))
:
Explicit description of a finset from its card #
theorem
Finset.exists_eq_insert_iff
{α : Type u_1}
[inst : DecidableEq α]
{s : Finset α}
{t : Finset α}
:
(∃ a x, insert a s = t) ↔ s ⊆ t ∧ Finset.card s + 1 = Finset.card t
theorem
Finset.card_le_one_iff_subset_singleton
{α : Type u_1}
{s : Finset α}
[inst : Nonempty α]
:
Finset.card s ≤ 1 ↔ ∃ x, s ⊆ {x}
theorem
Finset.card_le_one_of_subsingleton
{α : Type u_1}
[inst : Subsingleton α]
(s : Finset α)
:
Finset.card s ≤ 1
A Finset of a subsingleton type has cardinality at most one.
theorem
Finset.exists_ne_of_one_lt_card
{α : Type u_1}
{s : Finset α}
(hs : 1 < Finset.card s)
(a : α)
:
Inductions #
def
Finset.strongInduction
{α : 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
- Finset.strongInduction H x = H x fun t h => let_fun this := (_ : Finset.card t < Finset.card x); Finset.strongInduction H t
theorem
Finset.strongInduction_eq
{α : Type u_1}
{p : Finset α → Sort u_2}
(H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s)
(s : Finset α)
:
Finset.strongInduction H s = H s fun t x => Finset.strongInduction H t
Analogue of strongInduction with order of arguments swapped.
Equations
theorem
Finset.strongInductionOn_eq
{α : Type u_1}
{p : Finset α → Sort u_2}
(s : Finset α)
(H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s)
:
Finset.strongInductionOn s H = H s fun t x => Finset.strongInductionOn t H
def
Finset.strongDownwardInduction
{α : Type u_1}
{p : Finset α → Sort u_2}
{n : ℕ}
(H : (t₁ : Finset α) → ({t₂ : Finset α} → Finset.card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → Finset.card t₁ ≤ n → p t₁)
(s : Finset α)
:
Finset.card s ≤ 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} ht h => let_fun this := (_ : n - Finset.card t < n - Finset.card x); Finset.strongDownwardInduction H t ht
theorem
Finset.strongDownwardInduction_eq
{α : Type u_1}
{n : ℕ}
{p : Finset α → Sort u_2}
(H : (t₁ : Finset α) → ({t₂ : Finset α} → Finset.card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → Finset.card t₁ ≤ n → p t₁)
(s : Finset α)
:
Finset.strongDownwardInduction H s = H s fun {t} ht x => Finset.strongDownwardInduction H t ht
def
Finset.strongDownwardInductionOn
{α : Type u_1}
{n : ℕ}
{p : Finset α → Sort u_2}
(s : Finset α)
(H : (t₁ : Finset α) → ({t₂ : Finset α} → Finset.card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → Finset.card t₁ ≤ n → p t₁)
:
Finset.card s ≤ n → p s
Analogue of strongDownwardInduction with order of arguments swapped.
Equations
theorem
Finset.strongDownwardInductionOn_eq
{α : Type u_1}
{n : ℕ}
{p : Finset α → Sort u_2}
(s : Finset α)
(H : (t₁ : Finset α) → ({t₂ : Finset α} → Finset.card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → Finset.card t₁ ≤ n → p t₁)
:
(fun a => Finset.strongDownwardInductionOn s H a) = H s fun {t} ht x => Finset.strongDownwardInductionOn t H ht