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 PartENat.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 = PartENat.withTopEquiv ()
Instances For
@[simp]
theorem Set.encard_univ_coe {α : Type u_1} (s : Set α) :
Set.univ.encard = s.encard
theorem Set.encard_univ (α : Type u_3) :
Set.univ.encard = PartENat.withTopEquiv ()
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
theorem Set.encard_coe_eq_coe_finsetCard {α : Type u_1} (s : ) :
(s).encard = s.card
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
@[simp]
theorem Set.encard_singleton {α : Type u_1} (e : α) :
{e}.encard = 1
theorem Set.encard_union_eq {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) :
(s t).encard = s.encard + t.encard
theorem Set.encard_insert_of_not_mem {α : Type u_1} {s : Set α} {a : α} (has : as) :
(insert a s).encard = s.encard + 1
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 = (ENat.toNat s.encard)
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_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
theorem Set.encard_le_card {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
s.encard t.encard
theorem Set.encard_mono {α : Type u_3} :
Monotone Set.encard
theorem Set.encard_diff_add_encard_of_subset {α : Type u_1} {s : Set α} {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 : Set α) (t : Set α) :
(s \ t).encard + (s t).encard = s.encard
theorem Set.encard_union_add_encard_inter {α : Type u_1} (s : Set α) (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 : Set α} {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 : Set α} {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 : Set α} {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 : Set α) (t : Set α) :
(s t).encard s.encard + t.encard
theorem Set.finite_iff_finite_of_encard_eq_encard {α : Type u_1} {s : Set α} {t : Set α} (h : s.encard = t.encard) :
s.Finite t.Finite
theorem Set.infinite_iff_infinite_of_encard_eq_encard {α : Type u_1} {s : Set α} {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 : Set α} {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 : Set α} {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 : Set α} {t : Set α} (ht : t.Finite) (h : s t) :
s.encard < t.encard
theorem Set.encard_strictMono {α : Type u_1} [] :
StrictMono Set.encard
theorem Set.encard_diff_add_encard {α : Type u_1} (s : Set α) (t : Set α) :
(s \ t).encard + t.encard = (s t).encard
theorem Set.encard_le_encard_diff_add_encard {α : Type u_1} (s : Set α) (t : Set α) :
s.encard (s \ t).encard + t.encard
theorem Set.tsub_encard_le_encard_diff {α : Type u_1} (s : Set α) (t : Set α) :
s.encard - t.encard (s \ t).encard
theorem Set.encard_add_encard_compl {α : Type u_1} (s : Set α) :
s.encard + s.encard = Set.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 : as) (hb : b s) :
(insert a (s \ {b})).encard = s.encard
theorem Set.encard_exchange' {α : Type u_1} {s : Set α} {a : α} {b : α} (ha : as) (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 α), at 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 = as, (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 sb sa = b
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 : α) :
bs, 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.Nat.encard_range (k : ) :
{i : | i < k}.encard = k
theorem Set.Finite.eq_insert_of_subset_of_encard_eq_succ {α : Type u_1} {s : Set α} {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) :
ts, t.encard = k
theorem Set.exists_superset_subset_encard_eq {α : Type u_1} {s : Set α} {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 : ) :
(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 : ) (s : Set α) :
(f '' s).encard = s.encard
theorem Function.Embedding.enccard_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) :
theorem Set.encard_preimage_of_injective_subset_range {α : Type u_1} {β : Type u_2} {t : Set β} {f : αβ} (hf : ) (ht : t ) :
(f ⁻¹' t).encard = t.encard
theorem Set.encard_le_encard_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (hf : Set.MapsTo f s t) (f_inj : ) :
s.encard t.encard
@[irreducible]
theorem Set.Finite.exists_injOn_of_encard_le {α : Type u_1} {β : Type u_2} [] {s : Set α} {t : Set β} (hs : s.Finite) (hle : s.encard t.encard) :
∃ (f : αβ), s f ⁻¹' t
theorem Set.Finite.exists_bijOn_of_encard_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [] (hs : s.Finite) (h : s.encard = t.encard) :
∃ (f : αβ), Set.BijOn f s t

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

Equations
Instances For

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

Equations
Instances For
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 = ENat.toNat s.encard
Instances For
theorem Set.ncard_def {α : Type u_1} (s : Set α) :
s.ncard = ENat.toNat s.encard
theorem Set.Finite.cast_ncard_eq {α : Type u_1} {s : Set α} (hs : s.Finite) :
s.ncard = s.encard
theorem Set.Nat.card_coe_set_eq {α : Type u_1} (s : Set α) :
Nat.card s = s.ncard
theorem Set.ncard_eq_toFinset_card {α : Type u_1} (s : Set α) (hs : autoParam s.Finite _auto✝) :
s.ncard = ().card
theorem Set.ncard_eq_toFinset_card' {α : Type u_1} (s : Set α) [Fintype s] :
s.ncard = s.toFinset.card
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 : Set α} {t : Set α} (hst : s t) (ht : autoParam t.Finite _auto✝) :
s.ncard t.ncard
theorem Set.ncard_mono {α : Type u_1} [] :
Monotone Set.ncard
@[simp]
theorem Set.ncard_eq_zero {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
s.ncard = 0 s =
@[simp]
theorem Set.ncard_coe_Finset {α : Type u_1} (s : ) :
(s).ncard = s.card
theorem Set.ncard_univ (α : Type u_3) :
Set.univ.ncard =
@[simp]
theorem Set.ncard_empty (α : Type u_3) :
.ncard = 0
theorem Set.ncard_pos {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
0 < s.ncard s.Nonempty
theorem Set.ncard_ne_zero_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a s) (hs : autoParam s.Finite _auto✝) :
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_insert_of_not_mem {α : Type u_1} {s : Set α} {a : α} (h : as) (hs : autoParam s.Finite _auto✝) :
(insert a s).ncard = s.ncard + 1
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 : autoParam s.Finite _auto✝) :
(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
@[simp]
theorem Set.ncard_pair {α : Type u_1} {a : α} {b : α} (h : a b) :
{a, b}.ncard = 2
@[simp]
theorem Set.ncard_diff_singleton_add_one {α : Type u_1} {s : Set α} {a : α} (h : a s) (hs : autoParam s.Finite _auto✝) :
(s \ {a}).ncard + 1 = s.ncard
@[simp]
theorem Set.ncard_diff_singleton_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a s) (hs : autoParam s.Finite _auto✝) :
(s \ {a}).ncard = s.ncard - 1
theorem Set.ncard_diff_singleton_lt_of_mem {α : Type u_1} {s : Set α} {a : α} (h : a s) (hs : autoParam s.Finite _auto✝) :
(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 : as) (hb : b s) :
(insert a (s \ {b})).ncard = s.ncard
theorem Set.ncard_exchange' {α : Type u_1} {s : Set α} {a : α} {b : α} (ha : as) (hb : b s) :
(insert a s \ {b}).ncard = s.ncard
theorem Set.ncard_image_le {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (hs : autoParam s.Finite _auto✝) :
(f '' s).ncard s.ncard
theorem Set.ncard_image_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (H : ) :
(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 : autoParam s.Finite _auto✝) :
theorem Set.ncard_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (hs : autoParam s.Finite _auto✝) :
(f '' s).ncard = s.ncard
theorem Set.ncard_image_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} (s : Set α) (H : ) :
(f '' s).ncard = s.ncard
theorem Set.ncard_preimage_of_injective_subset_range {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} (H : ) (hs : s ) :
(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 : autoParam s.Finite _auto✝) :
{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 : | x s}.ncard = (s ).ncard
theorem Set.ncard_inter_le_ncard_left {α : Type u_1} (s : Set α) (t : Set α) (hs : autoParam s.Finite _auto✝) :
(s t).ncard s.ncard
theorem Set.ncard_inter_le_ncard_right {α : Type u_1} (s : Set α) (t : Set α) (ht : autoParam t.Finite _auto✝) :
(s t).ncard t.ncard
theorem Set.eq_of_subset_of_ncard_le {α : Type u_1} {s : Set α} {t : Set α} (h : s t) (h' : t.ncard s.ncard) (ht : autoParam t.Finite _auto✝) :
s = t
theorem Set.subset_iff_eq_of_ncard_le {α : Type u_1} {s : Set α} {t : Set α} (h : t.ncard s.ncard) (ht : autoParam t.Finite _auto✝) :
s t s = t
theorem Set.map_eq_of_subset {α : Type u_1} {s : Set α} {f : α α} (h : f '' s s) (hs : autoParam s.Finite _auto✝) :
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 : autoParam s.Finite _auto✝) :
P a
theorem Set.ncard_lt_ncard {α : Type u_1} {s : Set α} {t : Set α} (h : s t) (ht : autoParam t.Finite _auto✝) :
s.ncard < t.ncard
theorem Set.ncard_strictMono {α : Type u_1} [] :
StrictMono Set.ncard
theorem Set.ncard_eq_of_bijective {α : Type u_1} {s : Set α} {n : } (f : (i : ) → i < nα) (hf : as, ∃ (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 hji = 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 hba = b) (h₃ : bt, ∃ (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 : as, f a t) (f_inj : ) (ht : autoParam t.Finite _auto✝) :
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 : as, f a t) (ht : autoParam t.Finite _auto✝) :
xs, ys, x y f x = f y
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 ji = j) (hs : autoParam s.Finite _auto✝) :
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 : autoParam t.Finite _auto✝) (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 : bt, ∃ (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 : autoParam s.Finite _auto✝) :
a₁ = a₂
theorem Set.ncard_union_add_ncard_inter {α : Type u_1} (s : Set α) (t : Set α) (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
(s t).ncard + (s t).ncard = s.ncard + t.ncard
theorem Set.ncard_inter_add_ncard_union {α : Type u_1} (s : Set α) (t : Set α) (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
(s t).ncard + (s t).ncard = s.ncard + t.ncard
theorem Set.ncard_union_le {α : Type u_1} (s : Set α) (t : Set α) :
(s t).ncard s.ncard + t.ncard
theorem Set.ncard_union_eq {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
(s t).ncard = s.ncard + t.ncard
theorem Set.ncard_diff_add_ncard_of_subset {α : Type u_1} {s : Set α} {t : Set α} (h : s t) (ht : autoParam t.Finite _auto✝) :
(t \ s).ncard + s.ncard = t.ncard
theorem Set.ncard_diff {α : Type u_1} {s : Set α} {t : Set α} (h : s t) (ht : autoParam t.Finite _auto✝) :
(t \ s).ncard = t.ncard - s.ncard
theorem Set.ncard_le_ncard_diff_add_ncard {α : Type u_1} (s : Set α) (t : Set α) (ht : autoParam t.Finite _auto✝) :
s.ncard (s \ t).ncard + t.ncard
theorem Set.le_ncard_diff {α : Type u_1} (s : Set α) (t : Set α) (hs : autoParam s.Finite _auto✝) :
t.ncard - s.ncard (t \ s).ncard
theorem Set.ncard_diff_add_ncard {α : Type u_1} (s : Set α) (t : Set α) (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
(s \ t).ncard + t.ncard = (s t).ncard
theorem Set.diff_nonempty_of_ncard_lt_ncard {α : Type u_1} {s : Set α} {t : Set α} (h : s.ncard < t.ncard) (hs : autoParam s.Finite _auto✝) :
(t \ s).Nonempty
theorem Set.exists_mem_not_mem_of_ncard_lt_ncard {α : Type u_1} {s : Set α} {t : Set α} (h : s.ncard < t.ncard) (hs : autoParam s.Finite _auto✝) :
et, es
@[simp]
theorem Set.ncard_inter_add_ncard_diff_eq_ncard {α : Type u_1} (s : Set α) (t : Set α) (hs : autoParam s.Finite _auto✝) :
(s t).ncard + (s \ t).ncard = s.ncard
theorem Set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff {α : Type u_1} {s : Set α} {t : Set α} (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
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 : Set α} {t : Set α} (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
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 : Set α} {t : Set α} (hs : autoParam s.Finite _auto✝) (ht : autoParam t.Finite _auto✝) :
s.ncard < t.ncard (s \ t).ncard < (t \ s).ncard
theorem Set.ncard_add_ncard_compl {α : Type u_1} (s : Set α) (hs : autoParam s.Finite _auto✝) (hsc : autoParam s.Finite _auto✝) :
s.ncard + s.ncard =
theorem Set.exists_intermediate_Set {α : Type u_1} {s : Set α} {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 : Set α} {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) :
ts, 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 : ) :
ts, t.Finite t.ncard = k
theorem Set.Infinite.exists_superset_ncard_eq {α : Type u_1} {s : Set α} {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 : Set α} {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 : Set α} {t : Set α} (hs : autoParam s.Finite _auto✝) :
(as, insert a s = t) s t s.ncard + 1 = t.ncard
theorem Set.ncard_le_one {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
s.ncard 1 as, bs, a = b
theorem Set.ncard_le_one_iff {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
s.ncard 1 ∀ {a b : α}, a sb sa = b
theorem Set.ncard_le_one_iff_eq {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
s.ncard 1 s = ∃ (a : α), s = {a}
theorem Set.ncard_le_one_iff_subset_singleton {α : Type u_1} {s : Set α} [] (hs : autoParam s.Finite _auto✝) :
s.ncard 1 ∃ (x : α), s {x}
theorem Set.ncard_le_one_of_subsingleton {α : Type u_1} [] (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 : autoParam s.Finite _auto✝) :
1 < s.ncard as, bs, a b
theorem Set.one_lt_ncard_iff {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
1 < s.ncard ∃ (a : α) (b : α), a s b s a b
theorem Set.two_lt_ncard_iff {α : Type u_1} {s : Set α} (hs : autoParam s.Finite _auto✝) :
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 : autoParam s.Finite _auto✝) :
2 < s.ncard as, bs, cs, a b a c b c
theorem Set.exists_ne_of_one_lt_ncard {α : Type u_1} {s : Set α} (hs : 1 < s.ncard) (a : α) :
bs, b a
theorem Set.eq_insert_of_ncard_eq_succ {α : Type u_1} {s : Set α} {n : } (h : s.ncard = n + 1) :
∃ (a : α) (t : Set α), at insert a t = s t.ncard = n
theorem Set.ncard_eq_succ {α : Type u_1} {s : Set α} {n : } (hs : autoParam s.Finite _auto✝) :
s.ncard = n + 1 ∃ (a : α) (t : Set α), at 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}
@[deprecated Set.ncard_le_ncard]
theorem Set.ncard_le_of_subset {α : Type u_1} {s : Set α} {t : Set α} (hst : s t) (ht : autoParam t.Finite _auto✝) :
s.ncard t.ncard

Alias of Set.ncard_le_ncard.