Noncomputable Set Cardinality

We define the cardinality of set s as a term Set.encard s : ℕ∞ and a term Set.ncard s : ℕ. The latter takes the junk value of zero if s is infinite. Both functions are noncomputable, and are defined in terms of ENat.card (which takes a type as its argument); this file can be seen as an API for the same function in the special case where the type is a coercion of a Set, allowing for smoother interactions with the Set API.

Set.encard never takes junk values, so is more mathematically natural than Set.ncard, even though it takes values in a less convenient type. It is probably the right choice in settings where one is concerned with the cardinalities of sets that may or may not be infinite.

Set.ncard has a nicer codomain, but when using it, Set.Finite hypotheses are normally needed to make sure its values are meaningful. More generally, Set.ncard is intended to be used over the obvious alternative Finset.card when finiteness is 'propositional' rather than 'structural'. When working with sets that are finite by virtue of their definition, then Finset.card probably makes more sense. One setting where Set.ncard works nicely is in a type α with [Finite α], where every set is automatically finite. In this setting, we use default arguments and a simple tactic so that finiteness goals are discharged automatically in Set.ncard theorems.

Main Definitions

• Set.encard s is the cardinality of the set s as an extended natural number, with value ⊤ if s is infinite.
• 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.
• toFinite_tac is a tactic that tries to synthesize a Set.Finite s argument with Set.toFinite. This will work for s : Set α where there is a Finite α instance.

Implementation Notes

The theorems in this file are very similar to those in Data.Finset.Card, but with Set operations instead of Finset. We first prove all the theorems for Set.encard, and then derive most of the Set.ncard results as a consequence. Things are done this way to avoid reliance on the Finset API for theorems about infinite sets, and to allow for a refactor that removes or modifies Set.ncard in the future.

Nearly all the theorems for Set.ncard require finiteness of one or more of their arguments. We provide this assumption with a default argument of the form (hs : s.Finite := by toFinite_tac), where toFinite_tac will find an s.Finite 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 theorem, in which case we only include the ones that are needed, and derive the other inside the proof. A few of the theorems, such as ncard_union_le do not require finiteness arguments; they are true by coincidence due to junk values.

noncomputable def Set.encard {α : Type u_1} (s : Set α) : ℕ∞

The cardinality of a set as a term in ℕ∞

Equations

• s.encard = ENat.card ↑s

@[simp]

theorem Set.encard_univ (α : Type u_3) : univ.encard = ENat.card α

@[simp]

theorem ENat.card_coe_set_eq {α : Type u_1} (s : Set α) : card ↑s = s.encard

@[deprecated "Use simp" (since := "2025-09-23")]

theorem Set.encard_univ_coe {α : Type u_1} (s : Set α) : univ.encard = s.encard

theorem Set.Finite.encard_eq_coe_toFinset_card {α : Type u_1} {s : Set α} (h : s.Finite) : s.encard = ↑h.toFinset.card

theorem Set.encard_eq_coe_toFinset_card {α : Type u_1} (s : Set α) [Fintype ↑s] : s.encard = ↑s.toFinset.card

@[simp]

theorem Set.toENat_cardinalMk {α : Type u_1} (s : Set α) : Cardinal.toENat (Cardinal.mk ↑s) = s.encard

theorem Set.toENat_cardinalMk_subtype {α : Type u_1} (P : α → Prop) : Cardinal.toENat (Cardinal.mk { x : α // P x }) = {x : α | P x}.encard

@[simp]

theorem Set.coe_fintypeCard {α : Type u_1} (s : Set α) [Fintype ↑s] : ↑(Fintype.card ↑s) = s.encard

@[simp]

theorem Set.encard_coe_eq_coe_finsetCard {α : Type u_1} (s : Finset α) : (↑s).encard = ↑s.card

@[simp]

theorem Set.Infinite.encard_eq {α : Type u_1} {s : Set α} (h : s.Infinite) : s.encard = ⊤

@[simp]

theorem Set.encard_eq_zero {α : Type u_1} {s : Set α} : s.encard = 0 ↔ s = ∅

@[simp]

theorem Set.encard_empty {α : Type u_1} : ∅.encard = 0

theorem Set.nonempty_of_encard_ne_zero {α : Type u_1} {s : Set α} (h : s.encard ≠ 0) : s.Nonempty

theorem Set.encard_ne_zero {α : Type u_1} {s : Set α} : s.encard ≠ 0 ↔ s.Nonempty

@[simp]

theorem Set.encard_pos {α : Type u_1} {s : Set α} : 0 < s.encard ↔ s.Nonempty

theorem Set.Nonempty.encard_pos {α : Type u_1} {s : Set α} : s.Nonempty → 0 < s.encard

Alias of the reverse direction of Set.encard_pos.

@[simp]

theorem Set.encard_singleton {α : Type u_1} (e : α) : {e}.encard = 1

theorem Set.encard_union_eq {α : Type u_1} {s t : Set α} (h : Disjoint s t) : (s ∪ t).encard = s.encard + t.encard

theorem Set.encard_ne_add_one {α : Type u_1} (a : α) : {x : α | x ≠ a}.encard + 1 = ENat.card α

theorem Set.encard_insert_of_notMem {α : Type u_1} {s : Set α} {a : α} (has : a ∉ s) : (insert a s).encard = s.encard + 1

@[deprecated Set.encard_insert_of_notMem (since := "2025-05-23")]

theorem Set.encard_insert_of_not_mem {α : Type u_1} {s : Set α} {a : α} (has : a ∉ s) : (insert a s).encard = s.encard + 1

Alias of Set.encard_insert_of_notMem.

theorem Set.Finite.encard_lt_top {α : Type u_1} {s : Set α} (h : s.Finite) : s.encard < ⊤

theorem Set.Finite.encard_eq_coe {α : Type u_1} {s : Set α} (h : s.Finite) : s.encard = ↑s.encard.toNat

theorem Set.Finite.exists_encard_eq_coe {α : Type u_1} {s : Set α} (h : s.Finite) : ∃ (n : ℕ), s.encard = ↑n

@[simp]

theorem Set.encard_lt_top_iff {α : Type u_1} {s : Set α} : s.encard < ⊤ ↔ s.Finite

@[simp]

theorem Set.encard_eq_top_iff {α : Type u_1} {s : Set α} : s.encard = ⊤ ↔ s.Infinite

theorem Set.encard_eq_top {α : Type u_1} {s : Set α} : s.Infinite → s.encard = ⊤

Alias of the reverse direction of Set.encard_eq_top_iff.

theorem Set.encard_ne_top_iff {α : Type u_1} {s : Set α} : s.encard ≠ ⊤ ↔ s.Finite

theorem Set.finite_of_encard_le_coe {α : Type u_1} {s : Set α} {k : ℕ} (h : s.encard ≤ ↑k) : s.Finite

theorem Set.finite_of_encard_eq_coe {α : Type u_1} {s : Set α} {k : ℕ} (h : s.encard = ↑k) : s.Finite

theorem Set.encard_le_coe_iff {α : Type u_1} {s : Set α} {k : ℕ} : s.encard ≤ ↑k ↔ s.Finite ∧ ∃ (n₀ : ℕ), s.encard = ↑n₀ ∧ n₀ ≤ k

@[simp]

theorem Set.encard_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).encard = s.encard * t.encard

theorem Set.encard_le_encard {α : Type u_1} {s t : Set α} (h : s ⊆ t) : s.encard ≤ t.encard

theorem Set.encard_mono {α : Type u_3} : Monotone encard

theorem Set.encard_diff_add_encard_of_subset {α : Type u_1} {s t : Set α} (h : s ⊆ t) : (t \ s).encard + s.encard = t.encard

@[simp]

theorem Set.one_le_encard_iff_nonempty {α : Type u_1} {s : Set α} : 1 ≤ s.encard ↔ s.Nonempty

theorem Set.encard_diff_add_encard_inter {α : Type u_1} (s t : Set α) : (s \ t).encard + (s ∩ t).encard = s.encard

theorem Set.encard_union_add_encard_inter {α : Type u_1} (s t : Set α) : (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard

theorem Set.encard_eq_encard_iff_encard_diff_eq_encard_diff {α : Type u_1} {s t : Set α} (h : (s ∩ t).Finite) : s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard

theorem Set.encard_le_encard_iff_encard_diff_le_encard_diff {α : Type u_1} {s t : Set α} (h : (s ∩ t).Finite) : s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard

theorem Set.encard_lt_encard_iff_encard_diff_lt_encard_diff {α : Type u_1} {s t : Set α} (h : (s ∩ t).Finite) : s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard

theorem Set.encard_union_le {α : Type u_1} (s t : Set α) : (s ∪ t).encard ≤ s.encard + t.encard

theorem Set.finite_iff_finite_of_encard_eq_encard {α : Type u_1} {s t : Set α} (h : s.encard = t.encard) : s.Finite ↔ t.Finite

theorem Set.infinite_iff_infinite_of_encard_eq_encard {α : Type u_1} {s t : Set α} (h : s.encard = t.encard) : s.Infinite ↔ t.Infinite

theorem Set.Finite.finite_of_encard_le {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (h : t.encard ≤ s.encard) : t.Finite

theorem Set.Finite.eq_of_subset_of_encard_le' {α : Type u_1} {s t : Set α} (ht : t.Finite) (hst : s ⊆ t) (hts : t.encard ≤ s.encard) : s = t

theorem Set.Finite.eq_of_subset_of_encard_le {α : Type u_1} {s t : Set α} (hs : s.Finite) (hst : s ⊆ t) (hts : t.encard ≤ s.encard) : s = t

theorem Set.Finite.encard_lt_encard {α : Type u_1} {s t : Set α} (hs : s.Finite) (h : s ⊂ t) : s.encard < t.encard

theorem Set.encard_strictMono {α : Type u_1} [Finite α] : StrictMono encard

theorem Set.encard_diff_add_encard {α : Type u_1} (s t : Set α) : (s \ t).encard + t.encard = (s ∪ t).encard

theorem Set.encard_le_encard_diff_add_encard {α : Type u_1} (s t : Set α) : s.encard ≤ (s \ t).encard + t.encard

theorem Set.tsub_encard_le_encard_diff {α : Type u_1} (s t : Set α) : s.encard - t.encard ≤ (s \ t).encard

theorem Set.encard_add_encard_compl {α : Type u_1} (s : Set α) : s.encard + sᶜ.encard = univ.encard

theorem Set.encard_insert_le {α : Type u_1} (s : Set α) (x : α) : (insert x s).encard ≤ s.encard + 1

theorem Set.encard_singleton_inter {α : Type u_1} (s : Set α) (x : α) : ({x} ∩ s).encard ≤ 1

theorem Set.encard_diff_singleton_add_one {α : Type u_1} {s : Set α} {a : α} (h : a ∈ s) : (s \ {a}).encard + 1 = s.encard

theorem Set.encard_diff_singleton_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a ∈ s) : (s \ {a}).encard = s.encard - 1

theorem Set.encard_tsub_one_le_encard_diff_singleton {α : Type u_1} (s : Set α) (x : α) : s.encard - 1 ≤ (s \ {x}).encard

theorem Set.encard_exchange {α : Type u_1} {s : Set α} {a b : α} (ha : a ∉ s) (hb : b ∈ s) : (insert a (s \ {b})).encard = s.encard

theorem Set.encard_exchange' {α : Type u_1} {s : Set α} {a b : α} (ha : a ∉ s) (hb : b ∈ s) : (insert a s \ {b}).encard = s.encard

theorem Set.encard_eq_add_one_iff {α : Type u_1} {s : Set α} {k : ℕ∞} : s.encard = k + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k

theorem Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt {α : Type u_1} (s : Set α) : s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard

Every set is either empty, infinite, or can have its encard reduced by a removal. Intended for well-founded induction on the value of encard.

theorem Set.encard_pair {α : Type u_1} {x y : α} (hne : x ≠ y) : {x, y}.encard = 2

theorem Set.encard_eq_one {α : Type u_1} {s : Set α} : s.encard = 1 ↔ ∃ (x : α), s = {x}

theorem Set.encard_le_one_iff_eq {α : Type u_1} {s : Set α} : s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}

theorem Set.encard_le_one_iff {α : Type u_1} {s : Set α} : s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

theorem Set.encard_le_one_iff_subsingleton {α : Type u_1} {s : Set α} : s.encard ≤ 1 ↔ s.Subsingleton

theorem Set.one_lt_encard_iff_nontrivial {α : Type u_1} {s : Set α} : 1 < s.encard ↔ s.Nontrivial

theorem Set.one_lt_encard_iff {α : Type u_1} {s : Set α} : 1 < s.encard ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

theorem Set.exists_ne_of_one_lt_encard {α : Type u_1} {s : Set α} (h : 1 < s.encard) (a : α) : ∃ b ∈ s, b ≠ a

theorem Set.encard_eq_two {α : Type u_1} {s : Set α} : s.encard = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

theorem Set.encard_eq_three {α : Type u_1} {s : Set α} : s.encard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

theorem Set.encard_eq_four {α : Type u_1} {s : Set α} : s.encard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

theorem Set.Nat.encard_range (k : ℕ) : {i : ℕ | i < k}.encard = ↑k

theorem Set.Finite.eq_insert_of_subset_of_encard_eq_succ {α : Type u_1} {s t : Set α} (hs : s.Finite) (h : s ⊆ t) (hst : t.encard = s.encard + 1) : ∃ (a : α), t = insert a s

theorem Set.exists_subset_encard_eq {α : Type u_1} {s : Set α} {k : ℕ∞} (hk : k ≤ s.encard) : ∃ t ⊆ s, t.encard = k

theorem Set.exists_superset_subset_encard_eq {α : Type u_1} {s t : Set α} {k : ℕ∞} (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) : ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k

theorem Set.InjOn.encard_image {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : InjOn f s) : (f '' s).encard = s.encard

theorem Set.encard_congr {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) : s.encard = t.encard

theorem Function.Injective.encard_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) (s : Set α) : (f '' s).encard = s.encard

theorem Function.Injective.encard_range {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) : ENat.card α ≤ (Set.range f).encard

theorem Function.Embedding.encard_le {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ↪ ↑t) : s.encard ≤ t.encard

theorem Set.encard_image_le {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : (f '' s).encard ≤ s.encard

theorem Set.Finite.injOn_of_encard_image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hs : s.Finite) (h : (f '' s).encard = s.encard) : InjOn f s

theorem Set.encard_preimage_of_injective_subset_range {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} (hf : Function.Injective f) (ht : t ⊆ range f) : (f ⁻¹' t).encard = t.encard

theorem Set.encard_preimage_of_bijective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Bijective f) (t : Set β) : (f ⁻¹' t).encard = t.encard

theorem Set.encard_le_encard_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hf : MapsTo f s t) (f_inj : InjOn f s) : s.encard ≤ t.encard

theorem Set.encard_preimage_val_le_encard_left {α : Type u_1} (P Q : Set α) : (Subtype.val ⁻¹' Q).encard ≤ P.encard

theorem Set.encard_preimage_val_le_encard_right {α : Type u_1} (P Q : Set α) : (Subtype.val ⁻¹' Q).encard ≤ Q.encard

@[irreducible]

theorem Set.Finite.exists_injOn_of_encard_le {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set α} {t : Set β} (hs : s.Finite) (hle : s.encard ≤ t.encard) : ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

theorem Set.Finite.exists_bijOn_of_encard_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Nonempty β] (hs : s.Finite) (h : s.encard = t.encard) : ∃ (f : α → β), BijOn f s t

theorem Set.exists_ne_map_eq_of_encard_lt_of_maps_to {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hc : t.encard < s.encard) (hf : MapsTo f s t) : ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

A version of the pigeonhole principle for Sets rather than Finsets.

See also Finset.exists_ne_map_eq_of_card_lt_of_maps_to and Set.exists_ne_map_eq_of_ncard_lt_of_maps_to.

def Set.tacticToFinite_tac : Lean.ParserDescr

A tactic (for use in default params) that applies Set.toFinite to synthesize a Set.Finite term.

Equations

• Set.tacticToFinite_tac = Lean.ParserDescr.node `Set.tacticToFinite_tac 1024 (Lean.ParserDescr.nonReservedSymbol "toFinite_tac" false)

def Set.tacticTo_encard_tac : Lean.ParserDescr

A tactic useful for transferring proofs for encard to their corresponding card statements

Equations

• Set.tacticTo_encard_tac = Lean.ParserDescr.node `Set.tacticTo_encard_tac 1024 (Lean.ParserDescr.nonReservedSymbol "to_encard_tac" false)

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 = s.encard.toNat

theorem Set.ncard_def {α : Type u_1} (s : Set α) : s.ncard = s.encard.toNat

theorem Set.Finite.cast_ncard_eq {α : Type u_1} {s : Set α} (hs : s.Finite) : ↑s.ncard = s.encard

theorem Set.ncard_le_encard {α : Type u_1} (s : Set α) : ↑s.ncard ≤ s.encard

@[simp]

theorem Nat.card_coe_set_eq {α : Type u_1} (s : Set α) : Nat.card ↑s = s.ncard

@[deprecated Nat.card_coe_set_eq (since := "2025-07-05")]

theorem Set.Nat.card_coe_set_eq {α : Type u_1} (s : Set α) : Nat.card ↑s = s.ncard

Alias of Nat.card_coe_set_eq.

theorem Set.ncard_eq_toFinset_card {α : Type u_1} (s : Set α) (hs : s.Finite := by toFinite_tac) : s.ncard = hs.toFinset.card

theorem Set.ncard_eq_toFinset_card' {α : Type u_1} (s : Set α) [Fintype ↑s] : s.ncard = s.toFinset.card

theorem Set.cast_ncard {α : Type u_1} {s : Set α} (hs : s.Finite) : ↑s.ncard = Cardinal.mk ↑s

theorem Set.encard_le_coe_iff_finite_ncard_le {α : Type u_1} {s : Set α} {k : ℕ} : s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k

theorem Set.Infinite.ncard {α : Type u_1} {s : Set α} (hs : s.Infinite) : s.ncard = 0

theorem Set.ncard_le_ncard {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ t.ncard

theorem Set.ncard_mono {α : Type u_1} [Finite α] : Monotone ncard

@[simp]

theorem Set.ncard_eq_zero {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : s.ncard = 0 ↔ s = ∅

@[simp]

theorem Set.ncard_coe_finset {α : Type u_1} (s : Finset α) : (↑s).ncard = s.card

@[deprecated Set.ncard_coe_finset (since := "2025-07-05")]

theorem Set.ncard_coe_Finset {α : Type u_1} (s : Finset α) : (↑s).ncard = s.card

Alias of Set.ncard_coe_finset.

@[simp]

theorem Set.ncard_univ (α : Type u_3) : univ.ncard = Nat.card α

theorem Set.ncard_le_card {α : Type u_1} [Finite α] (s : Set α) : s.ncard ≤ Nat.card α

@[simp]

theorem Set.ncard_empty (α : Type u_3) : ∅.ncard = 0

theorem Set.ncard_pos {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 0 < s.ncard ↔ s.Nonempty

theorem Set.Nonempty.ncard_pos {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : s.Nonempty → 0 < s.ncard

Alias of the reverse direction of Set.ncard_pos.

theorem Set.ncard_ne_zero_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a ∈ s) (hs : s.Finite := by toFinite_tac) : s.ncard ≠ 0

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

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

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

@[simp]

theorem Set.ncard_singleton {α : Type u_1} (a : α) : {a}.ncard = 1

theorem Set.ncard_singleton_inter {α : Type u_1} (a : α) (s : Set α) : ({a} ∩ s).ncard ≤ 1

@[simp]

theorem Set.ncard_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).ncard = s.ncard * t.ncard

@[simp]

theorem Set.ncard_powerset {α : Type u_1} (s : Set α) (hs : s.Finite := by toFinite_tac) : (𝒫 s).ncard = 2 ^ s.ncard

@[simp]

theorem Set.ncard_insert_of_notMem {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s) (hs : s.Finite := by toFinite_tac) : (insert a s).ncard = s.ncard + 1

@[deprecated Set.ncard_insert_of_notMem (since := "2025-05-23")]

theorem Set.ncard_insert_of_not_mem {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s) (hs : s.Finite := by toFinite_tac) : (insert a s).ncard = s.ncard + 1

Alias of Set.ncard_insert_of_notMem.

theorem Set.ncard_insert_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a ∈ s) : (insert a s).ncard = s.ncard

theorem Set.ncard_insert_le {α : Type u_1} (a : α) (s : Set α) : (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 := by toFinite_tac) : (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

theorem Set.ncard_le_ncard_insert {α : Type u_1} (a : α) (s : Set α) : s.ncard ≤ (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 := by toFinite_tac) : (s \ {a}).ncard + 1 = s.ncard

@[simp]

theorem Set.ncard_diff_singleton_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a ∈ s) : (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 := by toFinite_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) : (insert a (s \ {b})).ncard = s.ncard

theorem Set.ncard_exchange' {α : Type u_1} {s : Set α} {a b : α} (ha : a ∉ s) (hb : b ∈ s) : (insert a s \ {b}).ncard = s.ncard

theorem Set.odd_card_insert_iff {α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) (hs : s.Finite := by toFinite_tac) : Odd (insert a s).ncard ↔ Even s.ncard

theorem Set.even_card_insert_iff {α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) (hs : s.Finite := by toFinite_tac) : Even (insert a s).ncard ↔ Odd s.ncard

theorem Set.ncard_image_le {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hs : s.Finite := by toFinite_tac) : (f '' s).ncard ≤ s.ncard

theorem Set.ncard_image_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (H : InjOn f s) : (f '' s).ncard = s.ncard

theorem Set.injOn_of_ncard_image_eq {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : (f '' s).ncard = s.ncard) (hs : s.Finite := by toFinite_tac) : InjOn f s

theorem Set.ncard_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hs : s.Finite := by toFinite_tac) : (f '' s).ncard = s.ncard ↔ InjOn 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 ⊆ 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 := by toFinite_tac) : {x : α | 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 ∩ setOf P).ncard

theorem Set.ncard_inter_le_ncard_left {α : Type u_1} (s t : Set α) (hs : s.Finite := by toFinite_tac) : (s ∩ t).ncard ≤ s.ncard

theorem Set.ncard_inter_le_ncard_right {α : Type u_1} (s t : Set α) (ht : t.Finite := by toFinite_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 := by toFinite_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 := by toFinite_tac) : s ⊆ t ↔ s = t

theorem Set.map_eq_of_subset {α : Type u_1} {s : Set α} {f : α ↪ α} (h : ⇑f '' s ⊆ s) (hs : s.Finite := by toFinite_tac) : ⇑f '' s = s

theorem Set.sep_of_ncard_eq {α : Type u_1} {s : Set α} {a : α} {P : α → Prop} (h : {x : α | x ∈ s ∧ P x}.ncard = s.ncard) (ha : a ∈ s) (hs : s.Finite := by toFinite_tac) : P a

theorem Set.ncard_lt_ncard {α : Type u_1} {s t : Set α} (h : s ⊂ t) (ht : t.Finite := by toFinite_tac) : s.ncard < t.ncard

theorem Set.ncard_lt_card {α : Type u_1} {s : Set α} [Finite α] (h : s ≠ univ) : s.ncard < Nat.card α

theorem Set.ncard_strictMono {α : Type u_1} [Finite α] : StrictMono ncard

theorem Set.ncard_eq_of_bijective {α : Type u_1} {s : Set α} {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.ncard = n

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

theorem Set.ncard_le_ncard_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : InjOn f s) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ t.ncard

theorem Set.ncard_range_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : (range f).ncard = Nat.card α

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 ∈ s, f a ∈ t) (ht : t.Finite := by toFinite_tac) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

A version of the pigeonhole principle for Sets rather than Finsets.

See also Finset.exists_ne_map_eq_of_card_lt_of_maps_to and Set.exists_ne_map_eq_of_encard_lt_of_maps_to.

theorem Set.le_ncard_of_inj_on_range {α : Type u_1} {s : Set α} {n : ℕ} (f : ℕ → α) (hf : ∀ i < n, f i ∈ s) (f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j) (hs : s.Finite := by toFinite_tac) : n ≤ s.ncard

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

theorem Set.ncard_coe {α : Type u_3} (s : Set α) : univ.ncard = s.ncard

@[simp]

theorem Set.ncard_graphOn {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β) : (graphOn f s).ncard = s.ncard

theorem Set.ncard_union_add_ncard_inter {α : Type u_1} (s t : Set α) (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_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 := by toFinite_tac) (ht : t.Finite := by toFinite_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 := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s ∪ t).ncard = s.ncard + t.ncard

theorem Set.ncard_union_eq_iff {α : Type u_1} {s t : Set α} (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t

theorem Set.ncard_union_lt {α : Type u_1} {s t : Set α} (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) (h : ¬Disjoint s t) : (s ∪ t).ncard < s.ncard + t.ncard

theorem Set.ncard_diff_add_ncard_of_subset {α : Type u_1} {s t : Set α} (h : s ⊆ t) (ht : t.Finite := by toFinite_tac) : (t \ s).ncard + s.ncard = t.ncard

theorem Set.ncard_diff {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (hs : s.Finite := by toFinite_tac) : (t \ s).ncard = t.ncard - s.ncard

theorem Set.cast_ncard_sdiff {α : Type u_1} {s t : Set α} {R : Type u_3} [AddGroupWithOne R] (hst : s ⊆ t) (ht : t.Finite) : ↑(t \ s).ncard = ↑t.ncard - ↑s.ncard

theorem Set.ncard_le_ncard_diff_add_ncard {α : Type u_1} (s t : Set α) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ (s \ t).ncard + t.ncard

theorem Set.le_ncard_diff {α : Type u_1} (s t : Set α) (hs : s.Finite := by toFinite_tac) : t.ncard - s.ncard ≤ (t \ s).ncard

theorem Set.ncard_diff_add_ncard {α : Type u_1} (s t : Set α) (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_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 := by toFinite_tac) : (t \ s).Nonempty

theorem Set.exists_mem_notMem_of_ncard_lt_ncard {α : Type u_1} {s t : Set α} (h : s.ncard < t.ncard) (hs : s.Finite := by toFinite_tac) : ∃ e ∈ t, e ∉ s

@[deprecated Set.exists_mem_notMem_of_ncard_lt_ncard (since := "2025-05-23")]

theorem Set.exists_mem_not_mem_of_ncard_lt_ncard {α : Type u_1} {s t : Set α} (h : s.ncard < t.ncard) (hs : s.Finite := by toFinite_tac) : ∃ e ∈ t, e ∉ s

Alias of Set.exists_mem_notMem_of_ncard_lt_ncard.

@[simp]

theorem Set.ncard_inter_add_ncard_diff_eq_ncard {α : Type u_1} (s t : Set α) (hs : s.Finite := by toFinite_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 := by toFinite_tac) (ht : t.Finite := by toFinite_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 := by toFinite_tac) (ht : t.Finite := by toFinite_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 := by toFinite_tac) (ht : t.Finite := by toFinite_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 := by toFinite_tac) (hsc : sᶜ.Finite := by toFinite_tac) : s.ncard + sᶜ.ncard = Nat.card α

theorem Set.eq_univ_iff_ncard {α : Type u_1} [Finite α] (s : Set α) : s = univ ↔ s.ncard = Nat.card α

theorem Set.even_ncard_compl_iff {α : Type u_1} [Finite α] (heven : Even (Nat.card α)) (s : Set α) : Even sᶜ.ncard ↔ Even s.ncard

theorem Set.odd_ncard_compl_iff {α : Type u_1} [Finite α] (heven : Even (Nat.card α)) (s : Set α) : Odd sᶜ.ncard ↔ Odd s.ncard

theorem Set.nonempty_inter_of_lt_ncard_add_ncard {α : Type u_1} {s t : Set α} [Finite α] (h : Nat.card α < s.ncard + t.ncard) : (s ∩ t).Nonempty

theorem Set.nonempty_inter_of_le_ncard_add_ncard {α : Type u_1} {s t : Set α} [Finite α] (h' : Nat.card α ≤ s.ncard + t.ncard) (h : s ∪ t ≠ univ) : (s ∩ t).Nonempty

theorem Set.union_ne_univ_of_ncard_add_ncard_lt {α : Type u_1} {s t : Set α} (h : s.ncard + t.ncard < Nat.card α) : s ∪ t ≠ univ

theorem Set.nonempty_inter_compl_of_ncard_add_ncard_lt {α : Type u_1} {s t : Set α} (h : s.ncard + t.ncard < Nat.card α) : (sᶜ ∩ tᶜ).Nonempty

theorem Set.exists_subsuperset_card_eq {α : Type u_1} {s t : Set α} {n : ℕ} (hst : s ⊆ t) (hsn : s.ncard ≤ n) (hnt : n ≤ t.ncard) : ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = 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 Set.exists_subset_card_eq {α : Type u_1} {s : Set α} {n : ℕ} (hns : n ≤ s.ncard) : ∃ t ⊆ s, t.ncard = n

We can shrink a set to any smaller size.

theorem Set.Infinite.exists_subset_ncard_eq {α : Type u_1} {s : Set α} (hs : s.Infinite) (k : ℕ) : ∃ t ⊆ s, t.Finite ∧ t.ncard = k

theorem Set.Infinite.exists_superset_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)

theorem Finset.exists_not_mem_of_card_lt_enatCard {α : Type u_1} {s : Finset α} (hs : ↑s.card < ENat.card α) : ∃ (a : α), a ∉ s

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 := by toFinite_tac) : (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

theorem Set.ncard_le_one {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

@[simp]

theorem Set.ncard_le_one_iff_subsingleton {α : Type u_1} {s : Set α} [Finite ↑s] : s.ncard ≤ 1 ↔ s.Subsingleton

theorem Set.ncard_le_one_iff {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_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 := by toFinite_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 := by toFinite_tac) : s.ncard ≤ 1 ↔ ∃ (x : α), s ⊆ {x}

theorem Set.ncard_le_one_of_subsingleton {α : Type u_1} [Subsingleton α] (s : Set α) : s.ncard ≤ 1

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

theorem Set.one_lt_ncard {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

theorem Set.one_lt_ncard_iff {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 1 < s.ncard ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

theorem Set.one_lt_ncard_of_nonempty_of_even {α : Type u_1} {s : Set α} (hs : s.Finite) (hn : s.Nonempty := by toFinite_tac) (he : Even s.ncard) : 1 < s.ncard

theorem Set.two_lt_ncard_iff {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 2 < s.ncard ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem Set.two_lt_ncard {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem Set.three_lt_ncard_iff {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 3 < s.ncard ↔ ∃ (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 Set.three_lt_ncard {α : Type u_1} {s : Set α} (hs : s.Finite := by toFinite_tac) : 3 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

theorem Set.exists_ne_of_one_lt_ncard {α : Type u_1} {s : Set α} (hs : 1 < s.ncard) (a : α) : ∃ 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 ∧ insert a t = s ∧ t.ncard = n

theorem Set.ncard_eq_succ {α : Type u_1} {s : Set α} {n : ℕ} (hs : s.Finite := by toFinite_tac) : s.ncard = n + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ 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}

theorem Set.ncard_eq_four {α : Type u_1} {s : Set α} : s.ncard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}