Documentation

Mathlib.Data.Set.Card

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 #

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
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 (PartENat.card α)
    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 : Finset α) :
    (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} [Finite α] :
    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 : Set.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 : Function.Injective f) (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 : Function.Injective f) (ht : t Set.range f) :
    (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 : Set.InjOn f s) :
    s.encard t.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 Set.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 : αβ), 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 = (Set.Finite.toFinset hs).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} [Finite α] :
          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 : Finset α) :
          (s).ncard = s.card
          theorem Set.ncard_univ (α : Type u_3) :
          Set.univ.ncard = Nat.card α
          @[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 : Set.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 : 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 Set.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 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 : 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 : Subtype P | x s}.ncard = (s setOf P).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} [Finite α] :
          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 : Set.InjOn f s) (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 = Nat.card α
          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 α} [Nonempty α] (hs : autoParam s.Finite _auto✝) :
          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 : 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.