mathlib3 documentation

data.set.ncard

Noncomputable Set Cardinality #

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

We define the cardinality set.ncard s of a set s as a natural number. This function is noncomputable (being defined in terms of nat.card) and takes the value 0 if s is infinite.

This can be seen as an API for nat.card α in the special case where α is a subtype arising from a set. It is intended as an alternative to finset.card and fintype.card, both of which contain data in their definition that can cause awkwardness when using set.to_finset. Using set.ncard allows cardinality computations to avoid finset/fintype completely, staying in set and letting finiteness be handled explicitly, or (where a finite α instance is present and the sets are in set α) via auto_params.

Main Definitions #

set.ncard s is the cardinality of the set s as a natural number, provided s is finite. If s is infinite, then set.ncard s = 0.
to_finite_tac is a tactic that tries to synthesize an set.finite s argument with set.to_finite. This will work for s : set α where there is a finite α instance.

Implementation Notes #

The lemmas in this file are very similar to those in data.finset.card, but with set operations instead of finset; most of the proofs invoke their finset analogues. Nearly all the lemmas require finiteness of one or more of their arguments. We provide this assumption with an auto_param argument of the form (hs : s.finite . to_finite_tac), where to_finite_tac will find a finite s term in the cases where s is a set in a finite type.

Often, where there are two set arguments s and t, the finiteness of one follows from the other in the context of the lemma, in which case we only include the ones that are needed, and derive the other inside the proof. A few of the lemmas, such as ncard_union_le do not require finiteness arguments; they are are true by coincidence due to junk values.

noncomputable def set.ncard {α : Type u_1} (s : set α) :

The cardinality of s : set α. Has the junk value 0 if s is infinite

Equations

s.ncard = nat.card ↥s

meta def set.to_finite_tac :

A tactic, for use in auto_params, that finds a t.finite term for a set t whose finiteness can be deduced from typeclasses (eg. in a finite type).

theorem set.ncard_def {α : Type u_1} (s : set α) :

s.ncard = nat.card ↥s

theorem set.ncard_eq_to_finset_card {α : Type u_1} (s : set α) (hs : s.finite . "to_finite_tac") :

s.ncard = (set.finite.to_finset hs).card

theorem set.ncard_le_of_subset {α : Type u_1} {s t : set α} (hst : s ⊆ t) (ht : t.finite . "to_finite_tac") :

s.ncard ≤ t.ncard

theorem set.ncard_mono {α : Type u_1} [finite α] :

monotone set.ncard

@[simp]

theorem set.ncard_eq_zero {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

s.ncard = 0 ↔ s = ∅

@[simp]

theorem set.ncard_coe_finset {α : Type u_1} (s : finset α) :

↑s.ncard = s.card

theorem set.infinite.ncard {α : Type u_1} {s : set α} (hs : s.infinite) :

theorem set.ncard_univ (α : Type u_1) :

set.univ.ncard = nat.card α

@[simp]

theorem set.ncard_empty (α : Type u_1) :

theorem set.ncard_pos {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

0 < s.ncard ↔ s.nonempty

theorem set.ncard_ne_zero_of_mem {α : Type u_1} {s : set α} {a : α} (h : a ∈ s) (hs : s.finite . "to_finite_tac") :

theorem set.finite_of_ncard_ne_zero {α : Type u_1} {s : set α} (hs : s.ncard ≠ 0) :

theorem set.finite_of_ncard_pos {α : Type u_1} {s : set α} (hs : 0 < s.ncard) :

theorem set.nonempty_of_ncard_ne_zero {α : Type u_1} {s : set α} (hs : s.ncard ≠ 0) :

@[simp]

theorem set.ncard_singleton {α : Type u_1} (a : α) :

{a}.ncard = 1

theorem set.ncard_singleton_inter {α : Type u_1} {s : set α} {a : α} :

({a} ∩ s).ncard ≤ 1

@[simp]

theorem set.ncard_insert_of_not_mem {α : Type u_1} {s : set α} {a : α} (h : a ∉ s) (hs : s.finite . "to_finite_tac") :

(has_insert.insert a s).ncard = s.ncard + 1

theorem set.ncard_insert_of_mem {α : Type u_1} {s : set α} {a : α} (h : a ∈ s) :

(has_insert.insert a s).ncard = s.ncard

theorem set.ncard_insert_le {α : Type u_1} (a : α) (s : set α) :

(has_insert.insert a s).ncard ≤ s.ncard + 1

theorem set.ncard_insert_eq_ite {α : Type u_1} {s : set α} {a : α} [decidable (a ∈ s)] (hs : s.finite . "to_finite_tac") :

(has_insert.insert a s).ncard = ite (a ∈ s) s.ncard (s.ncard + 1)

theorem set.ncard_le_ncard_insert {α : Type u_1} (a : α) (s : set α) :

s.ncard ≤ (has_insert.insert a s).ncard

theorem set.ncard_pair {α : Type u_1} {a b : α} (h : a ≠ b) :

{a, b}.ncard = 2

theorem set.ncard_diff_singleton_add_one {α : Type u_1} {s : set α} {a : α} (h : a ∈ s) (hs : s.finite . "to_finite_tac") :

(s \ {a}).ncard + 1 = s.ncard

theorem set.ncard_diff_singleton_of_mem {α : Type u_1} {s : set α} {a : α} (h : a ∈ s) (hs : s.finite . "to_finite_tac") :

(s \ {a}).ncard = s.ncard - 1

theorem set.ncard_diff_singleton_lt_of_mem {α : Type u_1} {s : set α} {a : α} (h : a ∈ s) (hs : s.finite . "to_finite_tac") :

(s \ {a}).ncard < s.ncard

theorem set.ncard_diff_singleton_le {α : Type u_1} (s : set α) (a : α) :

(s \ {a}).ncard ≤ s.ncard

theorem set.pred_ncard_le_ncard_diff_singleton {α : Type u_1} (s : set α) (a : α) :

s.ncard - 1 ≤ (s \ {a}).ncard

theorem set.ncard_exchange {α : Type u_1} {s : set α} {a b : α} (ha : a ∉ s) (hb : b ∈ s) :

(has_insert.insert a (s \ {b})).ncard = s.ncard

theorem set.ncard_exchange' {α : Type u_1} {s : set α} {a b : α} (ha : a ∉ s) (hb : b ∈ s) :

(has_insert.insert a s \ {b}).ncard = s.ncard

theorem set.ncard_image_le {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} (hs : s.finite . "to_finite_tac") :

(f '' s).ncard ≤ s.ncard

theorem set.ncard_image_of_inj_on {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} (H : set.inj_on f s) :

(f '' s).ncard = s.ncard

theorem set.inj_on_of_ncard_image_eq {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} (h : (f '' s).ncard = s.ncard) (hs : s.finite . "to_finite_tac") :

theorem set.ncard_image_iff {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} (hs : s.finite . "to_finite_tac") :

(f '' s).ncard = s.ncard ↔ set.inj_on f s

theorem set.ncard_image_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (s : set α) (H : function.injective f) :

(f '' s).ncard = s.ncard

theorem set.ncard_preimage_of_injective_subset_range {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} (H : function.injective f) (hs : s ⊆ set.range f) :

(f ⁻¹' s).ncard = s.ncard

theorem set.fiber_ncard_ne_zero_iff_mem_image {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} {y : β} (hs : s.finite . "to_finite_tac") :

{x ∈ s | f x = y}.ncard ≠ 0 ↔ y ∈ f '' s

@[simp]

theorem set.ncard_map {α : Type u_1} {β : Type u_2} {s : set α} (f : α ↪ β) :

(⇑f '' s).ncard = s.ncard

@[simp]

theorem set.ncard_subtype {α : Type u_1} (P : α → Prop) (s : set α) :

{x : subtype P | ↑x ∈ s}.ncard = (s ∩ set_of P).ncard

@[simp]

theorem set.nat.card_coe_set_eq {α : Type u_1} (s : set α) :

nat.card ↥s = s.ncard

theorem set.ncard_inter_le_ncard_left {α : Type u_1} (s t : set α) (hs : s.finite . "to_finite_tac") :

(s ∩ t).ncard ≤ s.ncard

theorem set.ncard_inter_le_ncard_right {α : Type u_1} (s t : set α) (ht : t.finite . "to_finite_tac") :

(s ∩ t).ncard ≤ t.ncard

theorem set.eq_of_subset_of_ncard_le {α : Type u_1} {s t : set α} (h : s ⊆ t) (h' : t.ncard ≤ s.ncard) (ht : t.finite . "to_finite_tac") :

s = t

theorem set.subset_iff_eq_of_ncard_le {α : Type u_1} {s t : set α} (h : t.ncard ≤ s.ncard) (ht : t.finite . "to_finite_tac") :

s ⊆ t ↔ s = t

theorem set.map_eq_of_subset {α : Type u_1} {s : set α} {f : α ↪ α} (h : ⇑f '' s ⊆ s) (hs : s.finite . "to_finite_tac") :

⇑f '' s = s

theorem set.sep_of_ncard_eq {α : Type u_1} {s : set α} {a : α} {P : α → Prop} (h : {x ∈ s | P x}.ncard = s.ncard) (ha : a ∈ s) (hs : s.finite . "to_finite_tac") :

P a

theorem set.ncard_lt_ncard {α : Type u_1} {s t : set α} (h : s ⊂ t) (ht : t.finite . "to_finite_tac") :

s.ncard < t.ncard

theorem set.ncard_strict_mono {α : Type u_1} [finite α] :

strict_mono set.ncard

theorem set.ncard_eq_of_bijective {α : Type u_1} {s : set α} {n : ℕ} (f : Π (i : ℕ), i < n → α) (hf : ∀ (a : α), a ∈ s → (∃ (i : ℕ) (h : i < n), f i h = a)) (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s) (f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) (hs : s.finite . "to_finite_tac") :

theorem set.ncard_congr {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (f : Π (a : α), a ∈ s → β) (h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t) (h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b) (h₃ : ∀ (b : β), b ∈ t → (∃ (a : α) (ha : a ∈ s), f a ha = b)) (hs : s.finite . "to_finite_tac") :

s.ncard = t.ncard

theorem set.ncard_le_ncard_of_inj_on {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (f : α → β) (hf : ∀ (a : α), a ∈ s → f a ∈ t) (f_inj : set.inj_on f s) (ht : t.finite . "to_finite_tac") :

s.ncard ≤ t.ncard

theorem set.exists_ne_map_eq_of_ncard_lt_of_maps_to {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (hc : t.ncard < s.ncard) {f : α → β} (hf : ∀ (a : α), a ∈ s → f a ∈ t) (ht : t.finite . "to_finite_tac") :

∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x ≠ y ∧ f x = f y

theorem set.le_ncard_of_inj_on_range {α : Type u_1} {s : set α} {n : ℕ} (f : ℕ → α) (hf : ∀ (i : ℕ), i < n → f i ∈ s) (f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j) (hs : s.finite . "to_finite_tac") :

theorem set.surj_on_of_inj_on_of_ncard_le {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (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.ncard ≤ s.ncard) (ht : t.finite . "to_finite_tac") (b : β) (H : b ∈ t) :

∃ (a : α) (ha : a ∈ s), b = f a ha

theorem set.inj_on_of_surj_on_of_ncard_le {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (f : Π (a : α), a ∈ s → β) (hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t) (hsurj : ∀ (b : β), b ∈ t → (∃ (a : α) (ha : a ∈ s), b = f a ha)) (hst : s.ncard ≤ t.ncard) ⦃a₁ a₂ : α⦄ (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s) (ha₁a₂ : f a₁ ha₁ = f a₂ ha₂) (hs : s.finite . "to_finite_tac") :

a₁ = a₂

theorem set.ncard_union_add_ncard_inter {α : Type u_1} (s t : set α) (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

(s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard

theorem set.ncard_inter_add_ncard_union {α : Type u_1} (s t : set α) (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

(s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard

theorem set.ncard_union_le {α : Type u_1} (s t : set α) :

(s ∪ t).ncard ≤ s.ncard + t.ncard

theorem set.ncard_union_eq {α : Type u_1} {s t : set α} (h : disjoint s t) (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

(s ∪ t).ncard = s.ncard + t.ncard

theorem set.ncard_diff_add_ncard_eq_ncard {α : Type u_1} {s t : set α} (h : s ⊆ t) (ht : t.finite . "to_finite_tac") :

(t \ s).ncard + s.ncard = t.ncard

theorem set.ncard_diff {α : Type u_1} {s t : set α} (h : s ⊆ t) (ht : t.finite . "to_finite_tac") :

(t \ s).ncard = t.ncard - s.ncard

theorem set.ncard_le_ncard_diff_add_ncard {α : Type u_1} (s t : set α) (ht : t.finite . "to_finite_tac") :

s.ncard ≤ (s \ t).ncard + t.ncard

theorem set.le_ncard_diff {α : Type u_1} (s t : set α) (hs : s.finite . "to_finite_tac") :

t.ncard - s.ncard ≤ (t \ s).ncard

theorem set.ncard_diff_add_ncard {α : Type u_1} (s t : set α) (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

(s \ t).ncard + t.ncard = (s ∪ t).ncard

theorem set.diff_nonempty_of_ncard_lt_ncard {α : Type u_1} {s t : set α} (h : s.ncard < t.ncard) (hs : s.finite . "to_finite_tac") :

(t \ s).nonempty

theorem set.exists_mem_not_mem_of_ncard_lt_ncard {α : Type u_1} {s t : set α} (h : s.ncard < t.ncard) (hs : s.finite . "to_finite_tac") :

∃ (e : α), e ∈ t ∧ e ∉ s

@[simp]

theorem set.ncard_inter_add_ncard_diff_eq_ncard {α : Type u_1} (s t : set α) (hs : s.finite . "to_finite_tac") :

(s ∩ t).ncard + (s \ t).ncard = s.ncard

theorem set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff {α : Type u_1} {s t : set α} (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard

theorem set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff {α : Type u_1} {s t : set α} (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

theorem set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff {α : Type u_1} {s t : set α} (hs : s.finite . "to_finite_tac") (ht : t.finite . "to_finite_tac") :

s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard

theorem set.ncard_add_ncard_compl {α : Type u_1} (s : set α) (hs : s.finite . "to_finite_tac") (hsc : sᶜ.finite . "to_finite_tac") :

s.ncard + sᶜ.ncard = nat.card α

theorem set.exists_intermediate_set {α : Type u_1} {s t : set α} (i : ℕ) (h₁ : i + s.ncard ≤ t.ncard) (h₂ : s ⊆ t) :

∃ (r : set α), s ⊆ r ∧ r ⊆ t ∧ r.ncard = i + s.ncard

Given a set t and a set s inside it, we can shrink t to any appropriate size, and keep s inside it.

theorem set.exists_intermediate_set' {α : Type u_1} {s t : set α} {m : ℕ} (hs : s.ncard ≤ m) (ht : m ≤ t.ncard) (h : s ⊆ t) :

∃ (r : set α), s ⊆ r ∧ r ⊆ t ∧ r.ncard = m

theorem set.exists_smaller_set {α : Type u_1} (s : set α) (i : ℕ) (h₁ : i ≤ s.ncard) :

∃ (t : set α), t ⊆ s ∧ t.ncard = i

We can shrink s to any smaller size.

theorem set.infinite.exists_subset_ncard_eq {α : Type u_1} {s : set α} (hs : s.infinite) (k : ℕ) :

∃ (t : set α), t ⊆ s ∧ t.finite ∧ t.ncard = k

theorem set.infinite.exists_supset_ncard_eq {α : Type u_1} {s t : set α} (ht : t.infinite) (hst : s ⊆ t) (hs : s.finite) {k : ℕ} (hsk : s.ncard ≤ k) :

∃ (s' : set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

theorem set.exists_subset_or_subset_of_two_mul_lt_ncard {α : Type u_1} {s t : set α} {n : ℕ} (hst : 2 * n < (s ∪ t).ncard) :

∃ (r : set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Explicit description of a set from its cardinality #

@[simp]

theorem set.ncard_eq_one {α : Type u_1} {s : set α} :

s.ncard = 1 ↔ ∃ (a : α), s = {a}

theorem set.exists_eq_insert_iff_ncard {α : Type u_1} {s t : set α} (hs : s.finite . "to_finite_tac") :

(∃ (a : α) (H : a ∉ s), has_insert.insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

theorem set.ncard_le_one {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

s.ncard ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b

theorem set.ncard_le_one_iff {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

theorem set.ncard_le_one_iff_eq {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ (a : α), s = {a}

theorem set.ncard_le_one_iff_subset_singleton {α : Type u_1} {s : set α} [nonempty α] (hs : s.finite . "to_finite_tac") :

s.ncard ≤ 1 ↔ ∃ (x : α), s ⊆ {x}

theorem set.ncard_le_one_of_subsingleton {α : Type u_1} [subsingleton α] (s : set α) :

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

theorem set.one_lt_ncard {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

1 < s.ncard ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ s), a ≠ b

theorem set.one_lt_ncard_iff {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

1 < s.ncard ↔ ∃ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

theorem set.two_lt_ncard_iff {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

2 < s.ncard ↔ ∃ (a b c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem set.two_lt_card {α : Type u_1} {s : set α} (hs : s.finite . "to_finite_tac") :

2 < s.ncard ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ s) (c : α) (H : c ∈ s), a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem set.exists_ne_of_one_lt_ncard {α : Type u_1} {s : set α} (hs : 1 < s.ncard) (a : α) :

∃ (b : α), b ∈ s ∧ b ≠ a

theorem set.eq_insert_of_ncard_eq_succ {α : Type u_1} {s : set α} {n : ℕ} (h : s.ncard = n + 1) :

∃ (a : α) (t : set α), a ∉ t ∧ has_insert.insert a t = s ∧ t.ncard = n

theorem set.ncard_eq_succ {α : Type u_1} {s : set α} {n : ℕ} (hs : s.finite . "to_finite_tac") :

s.ncard = n + 1 ↔ ∃ (a : α) (t : set α), a ∉ t ∧ has_insert.insert a t = s ∧ t.ncard = n

theorem set.ncard_eq_two {α : Type u_1} {s : set α} :

s.ncard = 2 ↔ ∃ (x y : α), x ≠ y ∧ s = {x, y}

theorem set.ncard_eq_three {α : Type u_1} {s : set α} :

s.ncard = 3 ↔ ∃ (x y z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}